Metamath Proof Explorer

Theorem mplcoe5lem

Description: Lemma for mplcoe4 . (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplcoe2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
mplcoe2.m ⊢ ↑ = ( .g ‘ 𝐺 )
mplcoe2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mplcoe5.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplcoe5.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
mplcoe5.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
mplcoe5.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐼 )
Assertion mplcoe5lem ( 𝜑 → ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3 mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplcoe2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
7 mplcoe2.m ⊢ ↑ = ( .g ‘ 𝐺 )
8 mplcoe2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
9 mplcoe5.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 mplcoe5.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11 mplcoe5.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
12 mplcoe5.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐼 )
13 vex ⊢ 𝑥 ∈ V
14 eqid ⊢ ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) )
15 14 elrnmpt ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
16 13 15 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
17 vex ⊢ 𝑦 ∈ V
18 14 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
19 17 18 mp1i ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↔ ∃ 𝑘 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
20 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝑌 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑙 ) )
21 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑙 ) )
22 20 21 oveq12d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) )
23 22 eqeq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑦 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ↔ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ↔ ∃ 𝑙 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) )
25 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
26 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
27 6 26 mgpplusg ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝐺 )
28 27 eqcomi ⊢ ( +g ‘ 𝐺 ) = ( .r ‘ 𝑃 )
29 1 mplring ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
30 5 9 29 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Ring )
31 ringsrg ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ SRing )
32 30 31 syl ⊢ ( 𝜑 → 𝑃 ∈ SRing )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → 𝑃 ∈ SRing )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑃 ∈ SRing )
35 6 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
36 30 35 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → 𝐺 ∈ Mnd )
38 12 sseld ⊢ ( 𝜑 → ( 𝑙 ∈ 𝑆 → 𝑙 ∈ 𝐼 ) )
39 38 imdistani ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( 𝜑 ∧ 𝑙 ∈ 𝐼 ) )
40 2 psrbag ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑌 ∈ 𝐷 ↔ ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑌 “ ℕ ) ∈ Fin ) ) )
41 5 40 syl ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐷 ↔ ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑌 “ ℕ ) ∈ Fin ) ) )
42 10 41 mpbid ⊢ ( 𝜑 → ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑌 “ ℕ ) ∈ Fin ) )
43 42 simpld ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ℕ0 )
44 43 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑙 ) ∈ ℕ0 )
45 39 44 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑙 ) ∈ ℕ0 )
46 5 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → 𝐼 ∈ 𝑊 )
47 9 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → 𝑅 ∈ Ring )
48 12 sselda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → 𝑙 ∈ 𝐼 )
49 1 8 25 46 47 48 mvrcl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑙 ) ∈ ( Base ‘ 𝑃 ) )
50 6 25 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
51 50 7 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑌 ‘ 𝑙 ) ∈ ℕ0 ∧ ( 𝑉 ‘ 𝑙 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∈ ( Base ‘ 𝑃 ) )
52 37 45 49 51 syl3anc ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∈ ( Base ‘ 𝑃 ) )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∈ ( Base ‘ 𝑃 ) )
54 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝐼 ∈ 𝑊 )
55 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝑅 ∈ Ring )
56 12 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ 𝐼 )
57 1 8 25 54 55 56 mvrcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
58 57 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
59 43 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
60 56 59 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
61 60 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
62 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑙 ) ∈ ( Base ‘ 𝑃 ) )
63 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑙 ) ∈ ℕ0 )
64 fveq2 ⊢ ( 𝑥 = 𝑙 → ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑙 ) )
65 64 oveq2d ⊢ ( 𝑥 = 𝑙 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) )
66 64 oveq1d ⊢ ( 𝑥 = 𝑙 → ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
67 65 66 eqeq12d ⊢ ( 𝑥 = 𝑙 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ) )
68 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑉 ‘ 𝑦 ) = ( 𝑉 ‘ 𝑘 ) )
69 68 oveq1d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) )
70 68 oveq2d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) )
71 69 70 eqeq12d ⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
72 67 71 rspc2v ⊢ ( ( 𝑙 ∈ 𝐼 ∧ 𝑘 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
73 48 56 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) → ( 𝑙 ∈ 𝐼 ∧ 𝑘 ∈ 𝐼 ) )
74 72 73 syl11 ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) → ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
75 74 expd ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) → ( 𝜑 → ( ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) ) )
76 11 75 mpcom ⊢ ( 𝜑 → ( ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
77 76 impl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) )
78 25 28 6 7 34 58 62 63 77 srgpcomp ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) )
79 25 28 6 7 34 53 58 61 78 srgpcomp ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
80 oveq12 ⊢ ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) )
81 oveq12 ⊢ ( ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
82 81 ancoms ⊢ ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
83 80 82 eqeq12d ⊢ ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
84 79 83 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
85 84 expd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
86 85 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
87 86 com23 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
88 87 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
89 24 88 syl5bi ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
90 19 89 sylbid ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
91 90 com23 ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
92 16 91 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
93 92 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∧ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
94 93 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∀ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
95 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝐺 ∈ Mnd )
96 12 sseld ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑆 → 𝑘 ∈ 𝐼 ) )
97 96 imdistani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) )
98 97 59 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
99 57 50 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
100 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
101 100 7 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 ∧ ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐺 ) )
102 95 98 99 101 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐺 ) )
103 102 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) : 𝑆 ⟶ ( Base ‘ 𝐺 ) )
104 103 frnd ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( Base ‘ 𝐺 ) )
105 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
106 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
107 100 105 106 sscntz ⊢ ( ( ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( Base ‘ 𝐺 ) ∧ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∀ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
108 104 104 107 syl2anc ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∀ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
109 94 108 mpbird ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )