Theorem cayhamlem3

Description: Lemma for cayhamlem4 . (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	chcoeffeq.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	chcoeffeq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	chcoeffeq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	chcoeffeq.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
	chcoeffeq.r	⊢ × = ( .r ‘ 𝑌 )
	chcoeffeq.s	⊢ − = ( -g ‘ 𝑌 )
	chcoeffeq.0	⊢ 0 = ( 0g ‘ 𝑌 )
	chcoeffeq.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	chcoeffeq.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
	chcoeffeq.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
	chcoeffeq.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
	chcoeffeq.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
	chcoeffeq.1	⊢ 1 = ( 1r ‘ 𝐴 )
	chcoeffeq.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
	chcoeffeq.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
	cayhamlem.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
	cayhamlem.r	⊢ · = ( .r ‘ 𝐴 )
Assertion	cayhamlem3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chcoeffeq.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		chcoeffeq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		chcoeffeq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		chcoeffeq.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		chcoeffeq.r	⊢ × = ( .r ‘ 𝑌 )
6		chcoeffeq.s	⊢ − = ( -g ‘ 𝑌 )
7		chcoeffeq.0	⊢ 0 = ( 0g ‘ 𝑌 )
8		chcoeffeq.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9		chcoeffeq.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
10		chcoeffeq.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
11		chcoeffeq.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
12		chcoeffeq.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
13		chcoeffeq.1	⊢ 1 = ( 1r ‘ 𝐴 )
14		chcoeffeq.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15		chcoeffeq.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
16		cayhamlem.e1	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
17		cayhamlem.r	⊢ · = ( .r ‘ 𝐴 )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	chcoeffeq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) )
19		2fveq3	⊢ ( 𝑛 = 𝑙 → ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) )
20		fveq2	⊢ ( 𝑛 = 𝑙 → ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) )
21	20	oveq1d	⊢ ( 𝑛 = 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) )
22	19 21	eqeq12d	⊢ ( 𝑛 = 𝑙 → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ↔ ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) )
23	22	cbvralvw	⊢ ( ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ↔ ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) )
24		2fveq3	⊢ ( 𝑙 = 𝑛 → ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) )
25		fveq2	⊢ ( 𝑙 = 𝑛 → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) )
26	25	oveq1d	⊢ ( 𝑙 = 𝑛 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) )
27	24 26	eqeq12d	⊢ ( 𝑙 = 𝑛 → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ↔ ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
28	27	rspccva	⊢ ( ( ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) )
29		simprll	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) )
30		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
31	9 1 2 3 30	chpmatply1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
32	29 31	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
33	10 32	eqeltrid	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
34		eqid	⊢ ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐾 )
35		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
36	34 30 3 35	coe1f	⊢ ( 𝐾 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝐾 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
37	33 36	syl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( coe1 ‘ 𝐾 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
38		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
39		nn0ex	⊢ ℕ0 ∈ V
40	38 39	pm3.2i	⊢ ( ( Base ‘ 𝑅 ) ∈ V ∧ ℕ0 ∈ V )
41		elmapg	⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ℕ0 ∈ V ) → ( ( coe1 ‘ 𝐾 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ↔ ( coe1 ‘ 𝐾 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ) )
42	40 41	mp1i	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( coe1 ‘ 𝐾 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ↔ ( coe1 ‘ 𝐾 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ) )
43	37 42	mpbird	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( coe1 ‘ 𝐾 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) )
44		simpl	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑛 ∈ ℕ0 )
45	35 1 2 13 14 16 17	cayhamlem2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( ( coe1 ‘ 𝐾 ) ∈ ( ( Base ‘ 𝑅 ) ↑m ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
46	29 43 44 45	syl12anc	⊢ ( ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
47	46	adantl	⊢ ( ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
48		oveq2	⊢ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
49	48	adantr	⊢ ( ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ) → ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )
50	47 49	eqtr4d	⊢ ( ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ∧ ( 𝑛 ∈ ℕ0 ∧ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
51	50	exp32	⊢ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ( 𝑛 ∈ ℕ0 → ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
52	51	com12	⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
53	52	adantl	⊢ ( ( ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
54	28 53	mpd	⊢ ( ( ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
55	54	com12	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ( ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
56	55	impl	⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) = ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) )
57	56	mpteq2dva	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) )
58	57	oveq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )
59	58	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) )
60	23 59	biimtrid	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) )
61	60	reximdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) → ( ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) )
62	61	reximdva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) ) )
63	18 62	mpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ ( 𝑛 ↑ 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )