Metamath Proof Explorer

Theorem evls1fpws

Description: Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025)

Ref Expression
Hypotheses ressply1evl2.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
ressply1evl2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
ressply1evl2.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
ressply1evl2.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
ressply1evl2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
evls1fpws.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1fpws.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1fpws.y ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
evls1fpws.1 ⊢ · = ( .r ‘ 𝑆 )
evls1fpws.2 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
evls1fpws.a ⊢ 𝐴 = ( coe1 ‘ 𝑀 )
Assertion evls1fpws ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ressply1evl2.q ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 ressply1evl2.k ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 ressply1evl2.w ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 ressply1evl2.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 ressply1evl2.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
6 evls1fpws.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
7 evls1fpws.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8 evls1fpws.y ⊢ ( 𝜑 → 𝑀 ∈ 𝐵 )
9 evls1fpws.1 ⊢ · = ( .r ‘ 𝑆 )
10 evls1fpws.2 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
11 evls1fpws.a ⊢ 𝐴 = ( coe1 ‘ 𝑀 )
12 4 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
13 7 12 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
14 eqid ⊢ ( var1 ‘ 𝑈 ) = ( var1 ‘ 𝑈 )
15 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
16 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
17 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑊 ) ) = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
18 3 14 5 15 16 17 11 ply1coe ⊢ ( ( 𝑈 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 = ( 𝑊 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) )
19 13 8 18 syl2anc ⊢ ( 𝜑 → 𝑀 = ( 𝑊 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) )
20 19 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( 𝑄 ‘ ( 𝑊 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) ) )
21 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
22 eqid ⊢ ( 𝑆 ↑s 𝐾 ) = ( 𝑆 ↑s 𝐾 )
23 3 ply1lmod ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ LMod )
24 13 23 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑊 ∈ LMod )
26 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
27 11 5 3 26 coe1fvalcl ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ 𝑈 ) )
28 8 27 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ 𝑈 ) )
29 3 ply1sca ⊢ ( 𝑈 ∈ Ring → 𝑈 = ( Scalar ‘ 𝑊 ) )
30 13 29 syl ⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑊 ) )
31 30 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ 𝑈 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
33 28 32 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
34 16 5 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
35 3 ply1ring ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
36 13 35 syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑊 ∈ Ring )
38 16 ringmgp ⊢ ( 𝑊 ∈ Ring → ( mulGrp ‘ 𝑊 ) ∈ Mnd )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑊 ) ∈ Mnd )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
41 13 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑈 ∈ Ring )
42 14 3 5 vr1cl ⊢ ( 𝑈 ∈ Ring → ( var1 ‘ 𝑈 ) ∈ 𝐵 )
43 41 42 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( var1 ‘ 𝑈 ) ∈ 𝐵 )
44 34 17 39 40 43 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 )
45 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
46 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
47 5 45 15 46 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ∈ 𝐵 )
48 25 33 44 47 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ∈ 𝐵 )
49 ssidd ⊢ ( 𝜑 → ℕ0 ⊆ ℕ0 )
50 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ V )
51 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑗 ) )
52 oveq1 ⊢ ( 𝑘 = 𝑗 → ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) = ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) )
53 51 52 oveq12d ⊢ ( 𝑘 = 𝑗 → ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) )
54 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
55 11 5 3 54 coe1ae0 ⊢ ( 𝑀 ∈ 𝐵 → ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) )
56 8 55 syl ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) )
57 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) )
58 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → 𝑈 = ( Scalar ‘ 𝑊 ) )
59 58 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( 0g ‘ 𝑈 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
60 57 59 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
61 60 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) )
62 24 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → 𝑊 ∈ LMod )
63 36 38 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑊 ) ∈ Mnd )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( mulGrp ‘ 𝑊 ) ∈ Mnd )
65 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → 𝑗 ∈ ℕ0 )
66 13 42 syl ⊢ ( 𝜑 → ( var1 ‘ 𝑈 ) ∈ 𝐵 )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( var1 ‘ 𝑈 ) ∈ 𝐵 )
68 34 17 64 65 67 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 )
69 68 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 )
70 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
71 5 45 15 70 21 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) )
72 62 69 71 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) )
73 61 72 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) ∧ ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) )
74 73 ex ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) ) )
75 74 imim2d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑗 ∈ ℕ0 ) → ( ( 𝑖 < 𝑗 → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) ) ) )
76 75 ralimdva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) ) ) )
77 76 reximdva ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( 𝐴 ‘ 𝑗 ) = ( 0g ‘ 𝑈 ) ) → ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) ) ) )
78 56 77 mpd ⊢ ( 𝜑 → ∃ 𝑖 ∈ ℕ0 ∀ 𝑗 ∈ ℕ0 ( 𝑖 < 𝑗 → ( ( 𝐴 ‘ 𝑗 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑗 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑊 ) ) )
79 50 48 53 78 mptnn0fsuppd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) finSupp ( 0g ‘ 𝑊 ) )
80 1 2 3 21 4 22 5 6 7 48 49 79 evls1gsumadd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) ) = ( ( 𝑆 ↑s 𝐾 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑄 ‘ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) ) )
81 1 2 22 4 3 evls1rhm ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
82 6 7 81 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) )
84 eqid ⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
85 84 45 36 24 46 5 asclf ⊢ ( 𝜑 → ( algSc ‘ 𝑊 ) : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ 𝐵 )
86 85 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( algSc ‘ 𝑊 ) : ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⟶ 𝐵 )
87 86 33 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ 𝐵 )
88 eqid ⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
89 eqid ⊢ ( .r ‘ ( 𝑆 ↑s 𝐾 ) ) = ( .r ‘ ( 𝑆 ↑s 𝐾 ) )
90 5 88 89 rhmmul ⊢ ( ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) ∧ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ∈ 𝐵 ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 ) → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ( .r ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ( .r ‘ ( 𝑆 ↑s 𝐾 ) ) ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) )
91 83 87 44 90 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ( .r ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ( .r ‘ ( 𝑆 ↑s 𝐾 ) ) ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) )
92 4 subrgcrng ⊢ ( ( 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑈 ∈ CRing )
93 6 7 92 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
94 3 ply1assa ⊢ ( 𝑈 ∈ CRing → 𝑊 ∈ AssAlg )
95 93 94 syl ⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
96 95 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑊 ∈ AssAlg )
97 84 45 46 5 88 15 asclmul1 ⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ∈ 𝐵 ) → ( ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ( .r ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) )
98 96 33 44 97 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ( .r ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) = ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) )
99 98 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ( .r ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( 𝑄 ‘ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) )
100 eqid ⊢ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) = ( Base ‘ ( 𝑆 ↑s 𝐾 ) )
101 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑆 ∈ CRing )
102 2 fvexi ⊢ 𝐾 ∈ V
103 102 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐾 ∈ V )
104 5 100 rhmf ⊢ ( 𝑄 ∈ ( 𝑊 RingHom ( 𝑆 ↑s 𝐾 ) ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
105 83 104 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑄 : 𝐵 ⟶ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
106 105 87 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
107 105 44 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ∈ ( Base ‘ ( 𝑆 ↑s 𝐾 ) ) )
108 22 100 101 103 106 107 9 89 pwsmulrval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ( .r ‘ ( 𝑆 ↑s 𝐾 ) ) ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ∘f · ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) )
109 22 2 100 101 103 106 pwselbas ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) : 𝐾 ⟶ 𝐾 )
110 109 ffnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) Fn 𝐾 )
111 22 2 100 101 103 107 pwselbas ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) : 𝐾 ⟶ 𝐾 )
112 111 ffnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) Fn 𝐾 )
113 inidm ⊢ ( 𝐾 ∩ 𝐾 ) = 𝐾
114 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑆 ∈ CRing )
115 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
116 2 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐾 )
117 7 116 syl ⊢ ( 𝜑 → 𝑅 ⊆ 𝐾 )
118 4 2 ressbas2 ⊢ ( 𝑅 ⊆ 𝐾 → 𝑅 = ( Base ‘ 𝑈 ) )
119 117 118 syl ⊢ ( 𝜑 → 𝑅 = ( Base ‘ 𝑈 ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 = ( Base ‘ 𝑈 ) )
121 28 120 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ 𝑅 )
122 121 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑘 ) ∈ 𝑅 )
123 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ 𝐾 )
124 1 3 4 2 84 114 115 122 123 evls1scafv ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ‘ 𝑥 ) = ( 𝐴 ‘ 𝑘 ) )
125 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑘 ∈ ℕ0 )
126 1 4 3 14 2 17 10 114 115 125 123 evls1varpwval ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ‘ 𝑥 ) = ( 𝑘 ↑ 𝑥 ) )
127 110 112 103 103 113 124 126 offval ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ∘f · ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) )
128 108 127 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ ( 𝐴 ‘ 𝑘 ) ) ) ( .r ‘ ( 𝑆 ↑s 𝐾 ) ) ( 𝑄 ‘ ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) )
129 91 99 128 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑄 ‘ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) )
130 129 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( 𝑄 ‘ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) )
131 130 oveq2d ⊢ ( 𝜑 → ( ( 𝑆 ↑s 𝐾 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑄 ‘ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) ) = ( ( 𝑆 ↑s 𝐾 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )
132 eqid ⊢ ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) = ( 0g ‘ ( 𝑆 ↑s 𝐾 ) )
133 102 a1i ⊢ ( 𝜑 → 𝐾 ∈ V )
134 nn0ex ⊢ ℕ0 ∈ V
135 134 a1i ⊢ ( 𝜑 → ℕ0 ∈ V )
136 6 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
137 136 ringcmnd ⊢ ( 𝜑 → 𝑆 ∈ CMnd )
138 136 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → 𝑆 ∈ Ring )
139 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
140 139 116 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ⊆ 𝐾 )
141 140 121 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ 𝐾 )
142 141 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑘 ) ∈ 𝐾 )
143 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
144 143 2 mgpbas ⊢ 𝐾 = ( Base ‘ ( mulGrp ‘ 𝑆 ) )
145 143 ringmgp ⊢ ( 𝑆 ∈ Ring → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
146 136 145 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
147 146 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
148 144 10 147 125 123 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑘 ↑ 𝑥 ) ∈ 𝐾 )
149 2 9 138 142 148 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ∈ 𝐾 )
150 149 3impa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ∈ 𝐾 )
151 150 3com23 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ∈ 𝐾 )
152 151 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑘 ∈ ℕ0 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ∈ 𝐾 )
153 135 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ∈ V )
154 funmpt ⊢ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) )
155 154 a1i ⊢ ( 𝜑 → Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) )
156 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) ∈ V )
157 11 5 3 54 coe1sfi ⊢ ( 𝑀 ∈ 𝐵 → 𝐴 finSupp ( 0g ‘ 𝑈 ) )
158 8 157 syl ⊢ ( 𝜑 → 𝐴 finSupp ( 0g ‘ 𝑈 ) )
159 158 fsuppimpd ⊢ ( 𝜑 → ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ∈ Fin )
160 11 5 3 26 coe1f ⊢ ( 𝑀 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑈 ) )
161 8 160 syl ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑈 ) )
162 161 ffnd ⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
163 162 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → 𝐴 Fn ℕ0 )
164 134 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ℕ0 ∈ V )
165 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 0g ‘ 𝑈 ) ∈ V )
166 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) )
167 163 164 165 166 fvdifsupp ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐴 ‘ 𝑘 ) = ( 0g ‘ 𝑈 ) )
168 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
169 4 168 subrg0 ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
170 7 169 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
171 170 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
172 167 171 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐴 ‘ 𝑘 ) = ( 0g ‘ 𝑆 ) )
173 172 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑘 ) = ( 0g ‘ 𝑆 ) )
174 173 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) = ( ( 0g ‘ 𝑆 ) · ( 𝑘 ↑ 𝑥 ) ) )
175 136 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑆 ∈ Ring )
176 175 145 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → ( mulGrp ‘ 𝑆 ) ∈ Mnd )
177 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) )
178 177 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑘 ∈ ℕ0 )
179 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ∈ 𝐾 )
180 144 10 176 178 179 mulgnn0cld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → ( 𝑘 ↑ 𝑥 ) ∈ 𝐾 )
181 2 9 168 ringlz ⊢ ( ( 𝑆 ∈ Ring ∧ ( 𝑘 ↑ 𝑥 ) ∈ 𝐾 ) → ( ( 0g ‘ 𝑆 ) · ( 𝑘 ↑ 𝑥 ) ) = ( 0g ‘ 𝑆 ) )
182 175 180 181 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 0g ‘ 𝑆 ) · ( 𝑘 ↑ 𝑥 ) ) = ( 0g ‘ 𝑆 ) )
183 174 182 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) = ( 0g ‘ 𝑆 ) )
184 183 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( 0g ‘ 𝑆 ) ) )
185 fconstmpt ⊢ ( 𝐾 × { ( 0g ‘ 𝑆 ) } ) = ( 𝑥 ∈ 𝐾 ↦ ( 0g ‘ 𝑆 ) )
186 184 185 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) = ( 𝐾 × { ( 0g ‘ 𝑆 ) } ) )
187 137 cmnmndd ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
188 22 168 pws0g ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝐾 ∈ V ) → ( 𝐾 × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) )
189 187 133 188 syl2anc ⊢ ( 𝜑 → ( 𝐾 × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) )
190 189 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝐾 × { ( 0g ‘ 𝑆 ) } ) = ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) )
191 186 190 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) = ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) )
192 191 135 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) supp ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) )
193 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ∧ ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) ∈ V ) ∧ ( ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ∈ Fin ∧ ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) supp ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑈 ) ) ) ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) finSupp ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) )
194 153 155 156 159 192 193 syl32anc ⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) finSupp ( 0g ‘ ( 𝑆 ↑s 𝐾 ) ) )
195 22 2 132 133 135 137 152 194 pwsgsum ⊢ ( 𝜑 → ( ( 𝑆 ↑s 𝐾 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝑥 ∈ 𝐾 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )
196 80 131 195 3eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑊 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( .g ‘ ( mulGrp ‘ 𝑊 ) ) ( var1 ‘ 𝑈 ) ) ) ) ) ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )
197 20 196 eqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = ( 𝑥 ∈ 𝐾 ↦ ( 𝑆 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑥 ) ) ) ) ) )