Metamath Proof Explorer

Theorem pmatcollpw3fi1lem1

Description: Lemma 1 for pmatcollpw3fi1 . (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p 
|- P = ( Poly1 ` R )
pmatcollpw.c 
|- C = ( N Mat P )
pmatcollpw.b 
|- B = ( Base ` C )
pmatcollpw.m 
|- .* = ( .s ` C )
pmatcollpw.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpw.x 
|- X = ( var1 ` R )
pmatcollpw.t 
|- T = ( N matToPolyMat R )
pmatcollpw3.a 
|- A = ( N Mat R )
pmatcollpw3.d 
|- D = ( Base ` A )
pmatcollpw3fi1lem1.0 
|- .0. = ( 0g ` A )
pmatcollpw3fi1lem1.h 
|- H = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( G ` 0 ) , .0. ) )
Assertion pmatcollpw3fi1lem1 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpw.c 
 |-  C = ( N Mat P )
3 pmatcollpw.b 
 |-  B = ( Base ` C )
4 pmatcollpw.m 
 |-  .* = ( .s ` C )
5 pmatcollpw.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpw.x 
 |-  X = ( var1 ` R )
7 pmatcollpw.t 
 |-  T = ( N matToPolyMat R )
8 pmatcollpw3.a 
 |-  A = ( N Mat R )
9 pmatcollpw3.d 
 |-  D = ( Base ` A )
10 pmatcollpw3fi1lem1.0 
 |-  .0. = ( 0g ` A )
11 pmatcollpw3fi1lem1.h 
 |-  H = ( l e. ( 0 ... 1 ) |-> if ( l = 0 , ( G ` 0 ) , .0. ) )
12 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) )
13 1 2 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
14 ringmnd 
 |-  ( C e. Ring -> C e. Mnd )
15 13 14 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Mnd )
16 15 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> C e. Mnd )
17 ringcmn 
 |-  ( C e. Ring -> C e. CMnd )
18 13 17 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. CMnd )
19 18 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> C e. CMnd )
20 snfi 
 |-  { 0 } e. Fin
21 20 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> { 0 } e. Fin )
22 simplll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> N e. Fin )
23 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> R e. Ring )
24 elmapi 
 |-  ( G e. ( D ^m { 0 } ) -> G : { 0 } --> D )
25 24 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> G : { 0 } --> D )
26 25 ffvelcdmda 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( G ` n ) e. D )
27 elsni 
 |-  ( n e. { 0 } -> n = 0 )
28 0nn0 
 |-  0 e. NN0
29 27 28 eqeltrdi 
 |-  ( n e. { 0 } -> n e. NN0 )
30 29 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> n e. NN0 )
31 8 9 7 1 2 3 4 5 6 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( G ` n ) e. D /\ n e. NN0 ) ) -> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) e. B )
32 22 23 26 30 31 syl22anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) e. B )
33 32 ralrimiva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> A. n e. { 0 } ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) e. B )
34 3 19 21 33 gsummptcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) e. B )
35 eqid 
 |-  ( +g ` C ) = ( +g ` C )
36 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
37 3 35 36 mndrid 
 |-  ( ( C e. Mnd /\ ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) e. B ) -> ( ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ( +g ` C ) ( 0g ` C ) ) = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) )
38 16 34 37 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ( +g ` C ) ( 0g ` C ) ) = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) )
39 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
40 39 eqcomi 
 |-  { 0 } = ( 0 ... 0 )
41 40 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> { 0 } = ( 0 ... 0 ) )
42 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) /\ l = n ) -> l = n )
43 27 ad2antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) /\ l = n ) -> n = 0 )
44 42 43 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) /\ l = n ) -> l = 0 )
45 44 iftrued 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) /\ l = n ) -> if ( l = 0 , ( G ` 0 ) , .0. ) = ( G ` 0 ) )
46 fveq2 
 |-  ( n = 0 -> ( G ` n ) = ( G ` 0 ) )
47 46 eqcomd 
 |-  ( n = 0 -> ( G ` 0 ) = ( G ` n ) )
48 27 47 syl 
 |-  ( n e. { 0 } -> ( G ` 0 ) = ( G ` n ) )
49 48 ad2antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) /\ l = n ) -> ( G ` 0 ) = ( G ` n ) )
50 45 49 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) /\ l = n ) -> if ( l = 0 , ( G ` 0 ) , .0. ) = ( G ` n ) )
51 1nn0 
 |-  1 e. NN0
52 51 a1i 
 |-  ( n = 0 -> 1 e. NN0 )
53 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
54 52 53 eleqtrdi 
 |-  ( n = 0 -> 1 e. ( ZZ>= ` 0 ) )
55 eluzfz1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... 1 ) )
56 54 55 syl 
 |-  ( n = 0 -> 0 e. ( 0 ... 1 ) )
57 eleq1 
 |-  ( n = 0 -> ( n e. ( 0 ... 1 ) <-> 0 e. ( 0 ... 1 ) ) )
58 56 57 mpbird 
 |-  ( n = 0 -> n e. ( 0 ... 1 ) )
59 27 58 syl 
 |-  ( n e. { 0 } -> n e. ( 0 ... 1 ) )
60 59 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> n e. ( 0 ... 1 ) )
61 ffvelcdm 
 |-  ( ( G : { 0 } --> D /\ n e. { 0 } ) -> ( G ` n ) e. D )
62 61 ex 
 |-  ( G : { 0 } --> D -> ( n e. { 0 } -> ( G ` n ) e. D ) )
63 24 62 syl 
 |-  ( G e. ( D ^m { 0 } ) -> ( n e. { 0 } -> ( G ` n ) e. D ) )
64 63 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( n e. { 0 } -> ( G ` n ) e. D ) )
65 64 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( G ` n ) e. D )
66 11 50 60 65 fvmptd2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( H ` n ) = ( G ` n ) )
67 66 eqcomd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( G ` n ) = ( H ` n ) )
68 67 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( T ` ( G ` n ) ) = ( T ` ( H ` n ) ) )
69 68 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. { 0 } ) -> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) = ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) )
70 41 69 mpteq12dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) = ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) )
71 70 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) = ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) )
72 ovexd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( 0 + 1 ) e. _V )
73 3 36 mndidcl 
 |-  ( C e. Mnd -> ( 0g ` C ) e. B )
74 15 73 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) e. B )
75 74 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( 0g ` C ) e. B )
76 0p1e1 
 |-  ( 0 + 1 ) = 1
77 76 eqeq2i 
 |-  ( n = ( 0 + 1 ) <-> n = 1 )
78 ax-1ne0 
 |-  1 =/= 0
79 78 neii 
 |-  -. 1 = 0
80 eqeq1 
 |-  ( n = 1 -> ( n = 0 <-> 1 = 0 ) )
81 79 80 mtbiri 
 |-  ( n = 1 -> -. n = 0 )
82 77 81 sylbi 
 |-  ( n = ( 0 + 1 ) -> -. n = 0 )
83 82 ad2antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) /\ l = n ) -> -. n = 0 )
84 eqeq1 
 |-  ( l = n -> ( l = 0 <-> n = 0 ) )
85 84 notbid 
 |-  ( l = n -> ( -. l = 0 <-> -. n = 0 ) )
86 85 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) /\ l = n ) -> ( -. l = 0 <-> -. n = 0 ) )
87 83 86 mpbird 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) /\ l = n ) -> -. l = 0 )
88 87 iffalsed 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) /\ l = n ) -> if ( l = 0 , ( G ` 0 ) , .0. ) = .0. )
89 88 10 eqtrdi 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) /\ l = n ) -> if ( l = 0 , ( G ` 0 ) , .0. ) = ( 0g ` A ) )
90 51 a1i 
 |-  ( n = 1 -> 1 e. NN0 )
91 90 53 eleqtrdi 
 |-  ( n = 1 -> 1 e. ( ZZ>= ` 0 ) )
92 eluzfz2 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> 1 e. ( 0 ... 1 ) )
93 91 92 syl 
 |-  ( n = 1 -> 1 e. ( 0 ... 1 ) )
94 eleq1 
 |-  ( n = 1 -> ( n e. ( 0 ... 1 ) <-> 1 e. ( 0 ... 1 ) ) )
95 93 94 mpbird 
 |-  ( n = 1 -> n e. ( 0 ... 1 ) )
96 77 95 sylbi 
 |-  ( n = ( 0 + 1 ) -> n e. ( 0 ... 1 ) )
97 96 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> n e. ( 0 ... 1 ) )
98 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( 0g ` A ) e. _V )
99 11 89 97 98 fvmptd2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( H ` n ) = ( 0g ` A ) )
100 99 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( T ` ( H ` n ) ) = ( T ` ( 0g ` A ) ) )
101 8 fveq2i 
 |-  ( 0g ` A ) = ( 0g ` ( N Mat R ) )
102 2 fveq2i 
 |-  ( 0g ` C ) = ( 0g ` ( N Mat P ) )
103 7 1 101 102 0mat2pmat 
 |-  ( ( R e. Ring /\ N e. Fin ) -> ( T ` ( 0g ` A ) ) = ( 0g ` C ) )
104 103 ancoms 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 0g ` A ) ) = ( 0g ` C ) )
105 104 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( T ` ( 0g ` A ) ) = ( 0g ` C ) )
106 100 105 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( T ` ( H ` n ) ) = ( 0g ` C ) )
107 106 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) = ( ( n .^ X ) .* ( 0g ` C ) ) )
108 1 2 pmatlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. LMod )
109 108 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> C e. LMod )
110 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> R e. Ring )
111 eleq1 
 |-  ( n = 1 -> ( n e. NN0 <-> 1 e. NN0 ) )
112 90 111 mpbird 
 |-  ( n = 1 -> n e. NN0 )
113 77 112 sylbi 
 |-  ( n = ( 0 + 1 ) -> n e. NN0 )
114 113 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> n e. NN0 )
115 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
116 eqid 
 |-  ( Base ` P ) = ( Base ` P )
117 1 6 115 5 116 ply1moncl 
 |-  ( ( R e. Ring /\ n e. NN0 ) -> ( n .^ X ) e. ( Base ` P ) )
118 110 114 117 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( n .^ X ) e. ( Base ` P ) )
119 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
120 2 matsca2 
 |-  ( ( N e. Fin /\ P e. Ring ) -> P = ( Scalar ` C ) )
121 119 120 sylan2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> P = ( Scalar ` C ) )
122 121 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` C ) = P )
123 122 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( Scalar ` C ) ) = ( Base ` P ) )
124 123 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) <-> ( n .^ X ) e. ( Base ` P ) ) )
125 124 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) <-> ( n .^ X ) e. ( Base ` P ) ) )
126 118 125 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) )
127 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
128 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
129 127 4 128 36 lmodvs0 
 |-  ( ( C e. LMod /\ ( n .^ X ) e. ( Base ` ( Scalar ` C ) ) ) -> ( ( n .^ X ) .* ( 0g ` C ) ) = ( 0g ` C ) )
130 109 126 129 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( ( n .^ X ) .* ( 0g ` C ) ) = ( 0g ` C ) )
131 107 130 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n = ( 0 + 1 ) ) -> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) = ( 0g ` C ) )
132 3 16 72 75 131 gsumsnd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) = ( 0g ` C ) )
133 132 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( 0g ` C ) = ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) )
134 71 133 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ( +g ` C ) ( 0g ` C ) ) = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
135 38 134 eqtr3d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
136 135 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
137 12 136 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
138 137 3impa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
139 28 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> 0 e. NN0 )
140 simplll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. ( 0 ... ( 0 + 1 ) ) ) -> N e. Fin )
141 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. ( 0 ... ( 0 + 1 ) ) ) -> R e. Ring )
142 id 
 |-  ( G : { 0 } --> D -> G : { 0 } --> D )
143 c0ex 
 |-  0 e. _V
144 143 snid 
 |-  0 e. { 0 }
145 144 a1i 
 |-  ( G : { 0 } --> D -> 0 e. { 0 } )
146 142 145 ffvelcdmd 
 |-  ( G : { 0 } --> D -> ( G ` 0 ) e. D )
147 24 146 syl 
 |-  ( G e. ( D ^m { 0 } ) -> ( G ` 0 ) e. D )
148 147 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ l e. ( 0 ... 1 ) ) -> ( G ` 0 ) e. D )
149 8 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
150 9 10 ring0cl 
 |-  ( A e. Ring -> .0. e. D )
151 149 150 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. e. D )
152 151 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ l e. ( 0 ... 1 ) ) -> .0. e. D )
153 148 152 ifcld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ l e. ( 0 ... 1 ) ) -> if ( l = 0 , ( G ` 0 ) , .0. ) e. D )
154 153 11 fmptd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> H : ( 0 ... 1 ) --> D )
155 76 oveq2i 
 |-  ( 0 ... ( 0 + 1 ) ) = ( 0 ... 1 )
156 155 feq2i 
 |-  ( H : ( 0 ... ( 0 + 1 ) ) --> D <-> H : ( 0 ... 1 ) --> D )
157 154 156 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> H : ( 0 ... ( 0 + 1 ) ) --> D )
158 157 ffvelcdmda 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. ( 0 ... ( 0 + 1 ) ) ) -> ( H ` n ) e. D )
159 elfznn0 
 |-  ( n e. ( 0 ... ( 0 + 1 ) ) -> n e. NN0 )
160 159 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. ( 0 ... ( 0 + 1 ) ) ) -> n e. NN0 )
161 8 9 7 1 2 3 4 5 6 mat2pmatscmxcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( H ` n ) e. D /\ n e. NN0 ) ) -> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) e. B )
162 140 141 158 160 161 syl22anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) /\ n e. ( 0 ... ( 0 + 1 ) ) ) -> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) e. B )
163 3 35 19 139 162 gsummptfzsplit 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) ) -> ( C gsum ( n e. ( 0 ... ( 0 + 1 ) ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
164 163 3adant3 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> ( C gsum ( n e. ( 0 ... ( 0 + 1 ) ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) = ( ( C gsum ( n e. ( 0 ... 0 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ( +g ` C ) ( C gsum ( n e. { ( 0 + 1 ) } |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) ) )
165 138 164 eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. ( 0 ... ( 0 + 1 ) ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) )
166 155 mpteq1i 
 |-  ( n e. ( 0 ... ( 0 + 1 ) ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) = ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) )
167 166 oveq2i 
 |-  ( C gsum ( n e. ( 0 ... ( 0 + 1 ) ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) )
168 165 167 eqtrdi 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ G e. ( D ^m { 0 } ) /\ M = ( C gsum ( n e. { 0 } |-> ( ( n .^ X ) .* ( T ` ( G ` n ) ) ) ) ) ) -> M = ( C gsum ( n e. ( 0 ... 1 ) |-> ( ( n .^ X ) .* ( T ` ( H ` n ) ) ) ) ) )