Metamath Proof Explorer

Theorem imasabl

Description: The image structure of an abelian group is an abelian group ( imasgrp analog). (Contributed by AV, 22-Feb-2025)

Ref Expression
Hypotheses imasabl.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
imasabl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
imasabl.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
imasabl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
imasabl.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
imasabl.r ⊢ ( 𝜑 → 𝑅 ∈ Abel )
imasabl.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion imasabl ( 𝜑 → ( 𝑈 ∈ Abel ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 imasabl.u ⊢ ( 𝜑 → 𝑈 = ( 𝐹 “s 𝑅 ) )
2 imasabl.v ⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3 imasabl.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
4 imasabl.f ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
5 imasabl.e ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
6 imasabl.r ⊢ ( 𝜑 → 𝑅 ∈ Abel )
7 imasabl.z ⊢ 0 = ( 0g ‘ 𝑅 )
8 6 ablgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
9 1 2 3 4 5 8 7 imasgrp ⊢ ( 𝜑 → ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
10 1 2 4 6 imasbas ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑈 ) )
11 10 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝑈 ) = 𝐵 )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑈 ) ↔ 𝑥 ∈ 𝐵 ) )
13 11 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ 𝑈 ) ↔ 𝑦 ∈ 𝐵 ) )
14 12 13 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) )
16 foelcdmi ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 )
17 16 ex ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ( 𝑥 ∈ 𝐵 → ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 ) )
18 foelcdmi ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 )
19 18 ex ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ( 𝑦 ∈ 𝐵 → ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 ) )
20 17 19 anim12d ⊢ ( 𝐹 : 𝑉 –onto→ 𝐵 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 ∧ ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) )
21 4 20 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 ∧ ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) )
22 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 ∧ ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 ) ) )
23 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → 𝑅 ∈ Abel )
24 2 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑉 ↔ 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
25 24 biimpd ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑉 → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( 𝑎 ∈ 𝑉 → 𝑎 ∈ ( Base ‘ 𝑅 ) ) )
27 26 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
28 27 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → 𝑎 ∈ ( Base ‘ 𝑅 ) )
29 2 eleq2d ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑉 ↔ 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
30 29 biimpd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑉 → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( 𝑏 ∈ 𝑉 → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) → ( 𝑏 ∈ 𝑉 → 𝑏 ∈ ( Base ‘ 𝑅 ) ) )
33 32 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ ( Base ‘ 𝑅 ) )
34 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
35 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
36 34 35 ablcom ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ∧ 𝑏 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑅 ) 𝑎 ) )
37 23 28 33 36 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) = ( 𝑏 ( +g ‘ 𝑅 ) 𝑎 ) )
38 37 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑅 ) 𝑎 ) ) )
39 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → 𝜑 )
40 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
41 40 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
42 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
43 3 eqcomd ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = + )
44 43 oveqd ⊢ ( 𝜑 → ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) = ( 𝑎 + 𝑏 ) )
45 44 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) )
46 43 oveqd ⊢ ( 𝜑 → ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) = ( 𝑝 + 𝑞 ) )
47 46 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) )
48 45 47 eqeq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ↔ ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
49 48 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ↔ ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
50 5 49 sylibrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 ( +g ‘ 𝑅 ) 𝑞 ) ) ) )
51 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
52 4 50 1 2 6 35 51 imasaddval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) )
53 39 41 42 52 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝐹 ‘ ( 𝑎 ( +g ‘ 𝑅 ) 𝑏 ) ) )
54 4 50 1 2 6 35 51 imasaddval ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑅 ) 𝑎 ) ) )
55 39 42 41 54 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 𝑏 ( +g ‘ 𝑅 ) 𝑎 ) ) )
56 38 53 55 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) )
57 56 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) ∧ ( ( 𝐹 ‘ 𝑏 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) )
58 oveq12 ⊢ ( ( ( 𝐹 ‘ 𝑎 ) = 𝑥 ∧ ( 𝐹 ‘ 𝑏 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) )
59 58 ancoms ⊢ ( ( ( 𝐹 ‘ 𝑏 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) → ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) )
60 oveq12 ⊢ ( ( ( 𝐹 ‘ 𝑏 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) → ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) )
61 59 60 eqeq12d ⊢ ( ( ( 𝐹 ‘ 𝑏 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) → ( ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) ↔ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) )
62 61 adantl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) ∧ ( ( 𝐹 ‘ 𝑏 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑏 ) ) = ( ( 𝐹 ‘ 𝑏 ) ( +g ‘ 𝑈 ) ( 𝐹 ‘ 𝑎 ) ) ↔ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) )
63 57 62 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) ∧ ( ( 𝐹 ‘ 𝑏 ) = 𝑦 ∧ ( 𝐹 ‘ 𝑎 ) = 𝑥 ) ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) )
64 63 exp32 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑏 ) = 𝑦 → ( ( 𝐹 ‘ 𝑎 ) = 𝑥 → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) ) )
65 64 rexlimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 → ( ( 𝐹 ‘ 𝑎 ) = 𝑥 → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) ) )
66 65 com23 ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑥 → ( ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) ) )
67 66 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 → ( ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) ) )
68 67 impd ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ( ∃ 𝑎 ∈ 𝑉 ( 𝐹 ‘ 𝑎 ) = 𝑥 ∧ ∃ 𝑏 ∈ 𝑉 ( 𝐹 ‘ 𝑏 ) = 𝑦 ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) )
69 22 68 syld ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) )
70 15 69 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) )
71 70 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑦 ∈ ( Base ‘ 𝑈 ) ) ) → ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) )
72 71 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) )
73 simpr ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
74 72 73 jca ⊢ ( ( 𝜑 ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) )
75 9 74 mpdan ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) )
76 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
77 76 51 isabl2 ⊢ ( 𝑈 ∈ Abel ↔ ( 𝑈 ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) )
78 77 anbi1i ⊢ ( ( 𝑈 ∈ Abel ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ↔ ( ( 𝑈 ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )
79 an21 ⊢ ( ( ( 𝑈 ∈ Grp ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ) ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) )
80 78 79 bitri ⊢ ( ( 𝑈 ∈ Abel ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑈 ) 𝑥 ) ∧ ( 𝑈 ∈ Grp ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) ) )
81 75 80 sylibr ⊢ ( 𝜑 → ( 𝑈 ∈ Abel ∧ ( 𝐹 ‘ 0 ) = ( 0g ‘ 𝑈 ) ) )