Metamath Proof Explorer

Theorem mhphflem

Description: Lemma for mhphf . Add several multiples of L together, in a case where the total amount of multiplies is N . (Contributed by SN, 30-Jul-2024)

Ref Expression
Hypotheses mhphflem.d 
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
mhphflem.h 
|- H = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
mhphflem.k 
|- B = ( Base ` G )
mhphflem.e 
|- .x. = ( .g ` G )
mhphflem.i 
|- ( ph -> I e. V )
mhphflem.g 
|- ( ph -> G e. Mnd )
mhphflem.l 
|- ( ph -> L e. B )
mhphflem.n 
|- ( ph -> N e. NN0 )
Assertion mhphflem 
|- ( ( ph /\ a e. H ) -> ( G gsum ( v e. I |-> ( ( a ` v ) .x. L ) ) ) = ( N .x. L ) )

Proof

Step Hyp Ref Expression
1 mhphflem.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
2 mhphflem.h 
 |-  H = { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N }
3 mhphflem.k 
 |-  B = ( Base ` G )
4 mhphflem.e 
 |-  .x. = ( .g ` G )
5 mhphflem.i 
 |-  ( ph -> I e. V )
6 mhphflem.g 
 |-  ( ph -> G e. Mnd )
7 mhphflem.l 
 |-  ( ph -> L e. B )
8 mhphflem.n 
 |-  ( ph -> N e. NN0 )
9 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
10 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
11 10 submbas 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> NN0 = ( Base ` ( CCfld |`s NN0 ) ) )
12 9 11 ax-mp 
 |-  NN0 = ( Base ` ( CCfld |`s NN0 ) )
13 cnfld0 
 |-  0 = ( 0g ` CCfld )
14 10 13 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s NN0 ) ) )
15 9 14 ax-mp 
 |-  0 = ( 0g ` ( CCfld |`s NN0 ) )
16 cnring 
 |-  CCfld e. Ring
17 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
18 16 17 ax-mp 
 |-  CCfld e. CMnd
19 10 submcmn 
 |-  ( ( CCfld e. CMnd /\ NN0 e. ( SubMnd ` CCfld ) ) -> ( CCfld |`s NN0 ) e. CMnd )
20 18 9 19 mp2an 
 |-  ( CCfld |`s NN0 ) e. CMnd
21 20 a1i 
 |-  ( ( ph /\ a e. H ) -> ( CCfld |`s NN0 ) e. CMnd )
22 6 adantr 
 |-  ( ( ph /\ a e. H ) -> G e. Mnd )
23 5 adantr 
 |-  ( ( ph /\ a e. H ) -> I e. V )
24 cnfldadd 
 |-  + = ( +g ` CCfld )
25 10 24 ressplusg 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> + = ( +g ` ( CCfld |`s NN0 ) ) )
26 9 25 ax-mp 
 |-  + = ( +g ` ( CCfld |`s NN0 ) )
27 eqid 
 |-  ( +g ` G ) = ( +g ` G )
28 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
29 10 submmnd 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> ( CCfld |`s NN0 ) e. Mnd )
30 9 29 mp1i 
 |-  ( ( ph /\ a e. H ) -> ( CCfld |`s NN0 ) e. Mnd )
31 6 ad2antrr 
 |-  ( ( ( ph /\ a e. H ) /\ n e. NN0 ) -> G e. Mnd )
32 simpr 
 |-  ( ( ( ph /\ a e. H ) /\ n e. NN0 ) -> n e. NN0 )
33 7 ad2antrr 
 |-  ( ( ( ph /\ a e. H ) /\ n e. NN0 ) -> L e. B )
34 3 4 mulgnn0cl 
 |-  ( ( G e. Mnd /\ n e. NN0 /\ L e. B ) -> ( n .x. L ) e. B )
35 31 32 33 34 syl3anc 
 |-  ( ( ( ph /\ a e. H ) /\ n e. NN0 ) -> ( n .x. L ) e. B )
36 35 fmpttd 
 |-  ( ( ph /\ a e. H ) -> ( n e. NN0 |-> ( n .x. L ) ) : NN0 --> B )
37 6 ad2antrr 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> G e. Mnd )
38 simprl 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> x e. NN0 )
39 simprr 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> y e. NN0 )
40 7 ad2antrr 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> L e. B )
41 3 4 27 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( x e. NN0 /\ y e. NN0 /\ L e. B ) ) -> ( ( x + y ) .x. L ) = ( ( x .x. L ) ( +g ` G ) ( y .x. L ) ) )
42 37 38 39 40 41 syl13anc 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( x + y ) .x. L ) = ( ( x .x. L ) ( +g ` G ) ( y .x. L ) ) )
43 eqid 
 |-  ( n e. NN0 |-> ( n .x. L ) ) = ( n e. NN0 |-> ( n .x. L ) )
44 oveq1 
 |-  ( n = ( x + y ) -> ( n .x. L ) = ( ( x + y ) .x. L ) )
45 nn0addcl 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x + y ) e. NN0 )
46 45 adantl 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x + y ) e. NN0 )
47 ovexd 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( x + y ) .x. L ) e. _V )
48 43 44 46 47 fvmptd3 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` ( x + y ) ) = ( ( x + y ) .x. L ) )
49 oveq1 
 |-  ( n = x -> ( n .x. L ) = ( x .x. L ) )
50 ovexd 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x .x. L ) e. _V )
51 43 49 38 50 fvmptd3 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` x ) = ( x .x. L ) )
52 oveq1 
 |-  ( n = y -> ( n .x. L ) = ( y .x. L ) )
53 ovexd 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( y .x. L ) e. _V )
54 43 52 39 53 fvmptd3 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` y ) = ( y .x. L ) )
55 51 54 oveq12d 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( ( n e. NN0 |-> ( n .x. L ) ) ` x ) ( +g ` G ) ( ( n e. NN0 |-> ( n .x. L ) ) ` y ) ) = ( ( x .x. L ) ( +g ` G ) ( y .x. L ) ) )
56 42 48 55 3eqtr4d 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` ( x + y ) ) = ( ( ( n e. NN0 |-> ( n .x. L ) ) ` x ) ( +g ` G ) ( ( n e. NN0 |-> ( n .x. L ) ) ` y ) ) )
57 oveq1 
 |-  ( n = 0 -> ( n .x. L ) = ( 0 .x. L ) )
58 0nn0 
 |-  0 e. NN0
59 58 a1i 
 |-  ( ( ph /\ a e. H ) -> 0 e. NN0 )
60 ovexd 
 |-  ( ( ph /\ a e. H ) -> ( 0 .x. L ) e. _V )
61 43 57 59 60 fvmptd3 
 |-  ( ( ph /\ a e. H ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` 0 ) = ( 0 .x. L ) )
62 7 adantr 
 |-  ( ( ph /\ a e. H ) -> L e. B )
63 3 28 4 mulg0 
 |-  ( L e. B -> ( 0 .x. L ) = ( 0g ` G ) )
64 62 63 syl 
 |-  ( ( ph /\ a e. H ) -> ( 0 .x. L ) = ( 0g ` G ) )
65 61 64 eqtrd 
 |-  ( ( ph /\ a e. H ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` 0 ) = ( 0g ` G ) )
66 12 3 26 27 15 28 30 22 36 56 65 ismhmd 
 |-  ( ( ph /\ a e. H ) -> ( n e. NN0 |-> ( n .x. L ) ) e. ( ( CCfld |`s NN0 ) MndHom G ) )
67 elrabi 
 |-  ( a e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } -> a e. D )
68 67 2 eleq2s 
 |-  ( a e. H -> a e. D )
69 68 adantl 
 |-  ( ( ph /\ a e. H ) -> a e. D )
70 1 psrbagf 
 |-  ( a e. D -> a : I --> NN0 )
71 69 70 syl 
 |-  ( ( ph /\ a e. H ) -> a : I --> NN0 )
72 71 ffvelrnda 
 |-  ( ( ( ph /\ a e. H ) /\ v e. I ) -> ( a ` v ) e. NN0 )
73 71 feqmptd 
 |-  ( ( ph /\ a e. H ) -> a = ( v e. I |-> ( a ` v ) ) )
74 1 psrbagfsupp 
 |-  ( a e. D -> a finSupp 0 )
75 69 74 syl 
 |-  ( ( ph /\ a e. H ) -> a finSupp 0 )
76 73 75 eqbrtrrd 
 |-  ( ( ph /\ a e. H ) -> ( v e. I |-> ( a ` v ) ) finSupp 0 )
77 oveq1 
 |-  ( n = ( a ` v ) -> ( n .x. L ) = ( ( a ` v ) .x. L ) )
78 oveq1 
 |-  ( n = ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) -> ( n .x. L ) = ( ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) .x. L ) )
79 12 15 21 22 23 66 72 76 77 78 gsummhm2 
 |-  ( ( ph /\ a e. H ) -> ( G gsum ( v e. I |-> ( ( a ` v ) .x. L ) ) ) = ( ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) .x. L ) )
80 73 oveq2d 
 |-  ( ( ph /\ a e. H ) -> ( ( CCfld |`s NN0 ) gsum a ) = ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) )
81 oveq2 
 |-  ( g = a -> ( ( CCfld |`s NN0 ) gsum g ) = ( ( CCfld |`s NN0 ) gsum a ) )
82 81 eqeq1d 
 |-  ( g = a -> ( ( ( CCfld |`s NN0 ) gsum g ) = N <-> ( ( CCfld |`s NN0 ) gsum a ) = N ) )
83 82 2 elrab2 
 |-  ( a e. H <-> ( a e. D /\ ( ( CCfld |`s NN0 ) gsum a ) = N ) )
84 83 simprbi 
 |-  ( a e. H -> ( ( CCfld |`s NN0 ) gsum a ) = N )
85 84 adantl 
 |-  ( ( ph /\ a e. H ) -> ( ( CCfld |`s NN0 ) gsum a ) = N )
86 80 85 eqtr3d 
 |-  ( ( ph /\ a e. H ) -> ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) = N )
87 86 oveq1d 
 |-  ( ( ph /\ a e. H ) -> ( ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) .x. L ) = ( N .x. L ) )
88 79 87 eqtrd 
 |-  ( ( ph /\ a e. H ) -> ( G gsum ( v e. I |-> ( ( a ` v ) .x. L ) ) ) = ( N .x. L ) )