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 5 9 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
30 ringsrg ⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ SRing )
31 29 30 syl ⊢ ( 𝜑 → 𝑃 ∈ SRing )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → 𝑃 ∈ SRing )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → 𝑃 ∈ SRing )
34 6 25 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
35 6 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
36 29 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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑙 ) ∈ ℕ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 34 7 37 45 49 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∈ ( Base ‘ 𝑃 ) )
51 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∈ ( Base ‘ 𝑃 ) )
52 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝐼 ∈ 𝑊 )
53 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝑅 ∈ Ring )
54 12 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝑘 ∈ 𝐼 )
55 1 8 25 52 53 54 mvrcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
56 55 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
57 43 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
58 54 57 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
59 58 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
60 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑙 ) ∈ ( Base ‘ 𝑃 ) )
61 45 adantr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑙 ) ∈ ℕ0 )
62 fveq2 ⊢ ( 𝑥 = 𝑙 → ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑙 ) )
63 62 oveq2d ⊢ ( 𝑥 = 𝑙 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) )
64 62 oveq1d ⊢ ( 𝑥 = 𝑙 → ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
65 63 64 eqeq12d ⊢ ( 𝑥 = 𝑙 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ) )
66 fveq2 ⊢ ( 𝑦 = 𝑘 → ( 𝑉 ‘ 𝑦 ) = ( 𝑉 ‘ 𝑘 ) )
67 66 oveq1d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) )
68 66 oveq2d ⊢ ( 𝑦 = 𝑘 → ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) )
69 67 68 eqeq12d ⊢ ( 𝑦 = 𝑘 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
70 65 69 rspc2v ⊢ ( ( 𝑙 ∈ 𝐼 ∧ 𝑘 ∈ 𝐼 ) → ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
71 48 54 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) → ( 𝑙 ∈ 𝐼 ∧ 𝑘 ∈ 𝐼 ) )
72 70 71 syl11 ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) → ( ( 𝜑 ∧ ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
73 72 expd ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) → ( 𝜑 → ( ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) ) )
74 11 73 mpcom ⊢ ( 𝜑 → ( ( 𝑙 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) ) )
75 74 impl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑙 ) ) = ( ( 𝑉 ‘ 𝑙 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) )
76 25 28 6 7 33 56 60 61 75 srgpcomp ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑉 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) )
77 25 28 6 7 33 51 56 59 76 srgpcomp ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
78 oveq12 ⊢ ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) )
79 oveq12 ⊢ ( ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
80 79 ancoms ⊢ ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
81 78 80 eqeq12d ⊢ ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ↔ ( ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) = ( ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ( +g ‘ 𝐺 ) ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
82 77 81 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∧ 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
83 82 expd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) ∧ 𝑘 ∈ 𝑆 ) → ( 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
84 83 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
85 84 com23 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑆 ) → ( 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
86 85 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑙 ) ↑ ( 𝑉 ‘ 𝑙 ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
87 24 86 biimtrid ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑆 𝑦 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
88 19 87 sylbid ⊢ ( 𝜑 → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
89 88 com23 ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝑆 𝑥 = ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
90 16 89 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) )
91 90 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∧ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
92 91 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∀ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
93 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
94 36 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → 𝐺 ∈ Mnd )
95 12 sseld ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑆 → 𝑘 ∈ 𝐼 ) )
96 95 imdistani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) )
97 96 57 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
98 55 34 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝐺 ) )
99 93 7 94 97 98 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑆 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝐺 ) )
100 99 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) : 𝑆 ⟶ ( Base ‘ 𝐺 ) )
101 100 frnd ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( Base ‘ 𝐺 ) )
102 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
103 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
104 93 102 103 sscntz ⊢ ( ( ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( Base ‘ 𝐺 ) ∧ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( Base ‘ 𝐺 ) ) → ( ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∀ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
105 101 101 104 syl2anc ⊢ ( 𝜑 → ( ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∀ 𝑦 ∈ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
106 92 105 mpbird ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝑆 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )