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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
pmatcollpw3.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pmatcollpw3.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
pmatcollpw3fi1lem1.0 ⊢ 0 = ( 0g ‘ 𝐴 )
pmatcollpw3fi1lem1.h ⊢ 𝐻 = ( 𝑙 ∈ ( 0 ... 1 ) ↦ if ( 𝑙 = 0 , ( 𝐺 ‘ 0 ) , 0 ) )
Assertion pmatcollpw3fi1lem1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝐺 ∈ ( 𝐷 ↑m { 0 } ) ∧ 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) → 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 1 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) )

Proof

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