Metamath Proof Explorer

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 syl5bi ⊢ ( ( ( ( 𝑁 ∈ 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 ↦ ( ( 𝑛 ↑ 𝑀 ) · ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ) ) ) )