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	ffvelcdmda	⊢ ( ( ( ( 𝑁 ∈ 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		ffvelcdm	⊢ ( ( 𝐺 : { 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	ffvelcdmd	⊢ ( 𝐺 : { 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	ffvelcdmda	⊢ ( ( ( ( 𝑁 ∈ 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 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝐻 ‘ 𝑛 ) ) ) ) ) )