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