Hi!
I've been trying to demonstrate a specialization of amgm to the case
where the sequence is explicit and of length k (say k=3 since we
already have amgm2).
The crucial part is obviously to demonstrate that amgm's "sums" are
equal to an explicit sum or product of k=3 elements. I've started with
trying to prove a statement along the lines of:
```
( ph -> ( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( A + (
B + C ) ) )
```
But quickly realized how unsure I was how to represent F in amgm? Also
looking at set.mm I failed to find any theorem that would let me
decompose the `gsum` sequentially.
I was expecting to find something along the very broad lines of:
```
( CCfld gsum { { 1 , A } , { 1 , B } , { 1 , C } } ) = ( ( CCfld gsum
{ { 1 , A } , { 1 , B } } ) + ( CCfld gsum { { 1 , C } } ) )
```
Left with no clear path forward and a failure to find good examples in
set.mm, I revert to the community for help :)
Would any of you have indications on how to proceed with proving the
translation from a `gsum` format to ( `( A + ( B + C ) ) )`?
Thank you so much!
-stan
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CACZd_0xfzwMeo6Fhe5TurJHn%2BGDmg%3DobjD9NEw%3DFc9w4Hy%3DG7g%40mail.gmail.com.
