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 31 32 33 mulgnn0cld 
 |-  ( ( ( ph /\ a e. H ) /\ n e. NN0 ) -> ( n .x. L ) e. B )
35 34 fmpttd 
 |-  ( ( ph /\ a e. H ) -> ( n e. NN0 |-> ( n .x. L ) ) : NN0 --> B )
36 6 ad2antrr 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> G e. Mnd )
37 simprl 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> x e. NN0 )
38 simprr 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> y e. NN0 )
39 7 ad2antrr 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> L e. B )
40 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 ) ) )
41 36 37 38 39 40 syl13anc 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( x + y ) .x. L ) = ( ( x .x. L ) ( +g ` G ) ( y .x. L ) ) )
42 eqid 
 |-  ( n e. NN0 |-> ( n .x. L ) ) = ( n e. NN0 |-> ( n .x. L ) )
43 oveq1 
 |-  ( n = ( x + y ) -> ( n .x. L ) = ( ( x + y ) .x. L ) )
44 nn0addcl 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x + y ) e. NN0 )
45 44 adantl 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x + y ) e. NN0 )
46 ovexd 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( x + y ) .x. L ) e. _V )
47 42 43 45 46 fvmptd3 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` ( x + y ) ) = ( ( x + y ) .x. L ) )
48 oveq1 
 |-  ( n = x -> ( n .x. L ) = ( x .x. L ) )
49 ovexd 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( x .x. L ) e. _V )
50 42 48 37 49 fvmptd3 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` x ) = ( x .x. L ) )
51 oveq1 
 |-  ( n = y -> ( n .x. L ) = ( y .x. L ) )
52 ovexd 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( y .x. L ) e. _V )
53 42 51 38 52 fvmptd3 
 |-  ( ( ( ph /\ a e. H ) /\ ( x e. NN0 /\ y e. NN0 ) ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` y ) = ( y .x. L ) )
54 50 53 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 ) ) )
55 41 47 54 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 ) ) )
56 oveq1 
 |-  ( n = 0 -> ( n .x. L ) = ( 0 .x. L ) )
57 0nn0 
 |-  0 e. NN0
58 57 a1i 
 |-  ( ( ph /\ a e. H ) -> 0 e. NN0 )
59 ovexd 
 |-  ( ( ph /\ a e. H ) -> ( 0 .x. L ) e. _V )
60 42 56 58 59 fvmptd3 
 |-  ( ( ph /\ a e. H ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` 0 ) = ( 0 .x. L ) )
61 7 adantr 
 |-  ( ( ph /\ a e. H ) -> L e. B )
62 3 28 4 mulg0 
 |-  ( L e. B -> ( 0 .x. L ) = ( 0g ` G ) )
63 61 62 syl 
 |-  ( ( ph /\ a e. H ) -> ( 0 .x. L ) = ( 0g ` G ) )
64 60 63 eqtrd 
 |-  ( ( ph /\ a e. H ) -> ( ( n e. NN0 |-> ( n .x. L ) ) ` 0 ) = ( 0g ` G ) )
65 12 3 26 27 15 28 30 22 35 55 64 ismhmd 
 |-  ( ( ph /\ a e. H ) -> ( n e. NN0 |-> ( n .x. L ) ) e. ( ( CCfld |`s NN0 ) MndHom G ) )
66 elrabi 
 |-  ( a e. { g e. D | ( ( CCfld |`s NN0 ) gsum g ) = N } -> a e. D )
67 66 2 eleq2s 
 |-  ( a e. H -> a e. D )
68 67 adantl 
 |-  ( ( ph /\ a e. H ) -> a e. D )
69 1 psrbagf 
 |-  ( a e. D -> a : I --> NN0 )
70 68 69 syl 
 |-  ( ( ph /\ a e. H ) -> a : I --> NN0 )
71 70 ffvelcdmda 
 |-  ( ( ( ph /\ a e. H ) /\ v e. I ) -> ( a ` v ) e. NN0 )
72 70 feqmptd 
 |-  ( ( ph /\ a e. H ) -> a = ( v e. I |-> ( a ` v ) ) )
73 1 psrbagfsupp 
 |-  ( a e. D -> a finSupp 0 )
74 68 73 syl 
 |-  ( ( ph /\ a e. H ) -> a finSupp 0 )
75 72 74 eqbrtrrd 
 |-  ( ( ph /\ a e. H ) -> ( v e. I |-> ( a ` v ) ) finSupp 0 )
76 oveq1 
 |-  ( n = ( a ` v ) -> ( n .x. L ) = ( ( a ` v ) .x. L ) )
77 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 ) )
78 12 15 21 22 23 65 71 75 76 77 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 ) )
79 72 oveq2d 
 |-  ( ( ph /\ a e. H ) -> ( ( CCfld |`s NN0 ) gsum a ) = ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) )
80 oveq2 
 |-  ( g = a -> ( ( CCfld |`s NN0 ) gsum g ) = ( ( CCfld |`s NN0 ) gsum a ) )
81 80 eqeq1d 
 |-  ( g = a -> ( ( ( CCfld |`s NN0 ) gsum g ) = N <-> ( ( CCfld |`s NN0 ) gsum a ) = N ) )
82 81 2 elrab2 
 |-  ( a e. H <-> ( a e. D /\ ( ( CCfld |`s NN0 ) gsum a ) = N ) )
83 82 simprbi 
 |-  ( a e. H -> ( ( CCfld |`s NN0 ) gsum a ) = N )
84 83 adantl 
 |-  ( ( ph /\ a e. H ) -> ( ( CCfld |`s NN0 ) gsum a ) = N )
85 79 84 eqtr3d 
 |-  ( ( ph /\ a e. H ) -> ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) = N )
86 85 oveq1d 
 |-  ( ( ph /\ a e. H ) -> ( ( ( CCfld |`s NN0 ) gsum ( v e. I |-> ( a ` v ) ) ) .x. L ) = ( N .x. L ) )
87 78 86 eqtrd 
 |-  ( ( ph /\ a e. H ) -> ( G gsum ( v e. I |-> ( ( a ` v ) .x. L ) ) ) = ( N .x. L ) )