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 
|- ( ph -> U = ( F "s R ) )
imasabl.v 
|- ( ph -> V = ( Base ` R ) )
imasabl.p 
|- ( ph -> .+ = ( +g ` R ) )
imasabl.f 
|- ( ph -> F : V -onto-> B )
imasabl.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
imasabl.r 
|- ( ph -> R e. Abel )
imasabl.z 
|- .0. = ( 0g ` R )
Assertion imasabl 
|- ( ph -> ( U e. Abel /\ ( F ` .0. ) = ( 0g ` U ) ) )

Proof

Step Hyp Ref Expression
1 imasabl.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasabl.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasabl.p 
 |-  ( ph -> .+ = ( +g ` R ) )
4 imasabl.f 
 |-  ( ph -> F : V -onto-> B )
5 imasabl.e 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
6 imasabl.r 
 |-  ( ph -> R e. Abel )
7 imasabl.z 
 |-  .0. = ( 0g ` R )
8 6 ablgrpd 
 |-  ( ph -> R e. Grp )
9 1 2 3 4 5 8 7 imasgrp 
 |-  ( ph -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )
10 1 2 4 6 imasbas 
 |-  ( ph -> B = ( Base ` U ) )
11 10 eqcomd 
 |-  ( ph -> ( Base ` U ) = B )
12 11 eleq2d 
 |-  ( ph -> ( x e. ( Base ` U ) <-> x e. B ) )
13 11 eleq2d 
 |-  ( ph -> ( y e. ( Base ` U ) <-> y e. B ) )
14 12 13 anbi12d 
 |-  ( ph -> ( ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) <-> ( x e. B /\ y e. B ) ) )
15 14 adantr 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) <-> ( x e. B /\ y e. B ) ) )
16 foelcdmi 
 |-  ( ( F : V -onto-> B /\ x e. B ) -> E. a e. V ( F ` a ) = x )
17 16 ex 
 |-  ( F : V -onto-> B -> ( x e. B -> E. a e. V ( F ` a ) = x ) )
18 foelcdmi 
 |-  ( ( F : V -onto-> B /\ y e. B ) -> E. b e. V ( F ` b ) = y )
19 18 ex 
 |-  ( F : V -onto-> B -> ( y e. B -> E. b e. V ( F ` b ) = y ) )
20 17 19 anim12d 
 |-  ( F : V -onto-> B -> ( ( x e. B /\ y e. B ) -> ( E. a e. V ( F ` a ) = x /\ E. b e. V ( F ` b ) = y ) ) )
21 4 20 syl 
 |-  ( ph -> ( ( x e. B /\ y e. B ) -> ( E. a e. V ( F ` a ) = x /\ E. b e. V ( F ` b ) = y ) ) )
22 21 adantr 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( ( x e. B /\ y e. B ) -> ( E. a e. V ( F ` a ) = x /\ E. b e. V ( F ` b ) = y ) ) )
23 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> R e. Abel )
24 2 eleq2d 
 |-  ( ph -> ( a e. V <-> a e. ( Base ` R ) ) )
25 24 biimpd 
 |-  ( ph -> ( a e. V -> a e. ( Base ` R ) ) )
26 25 adantr 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( a e. V -> a e. ( Base ` R ) ) )
27 26 imp 
 |-  ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) -> a e. ( Base ` R ) )
28 27 adantr 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> a e. ( Base ` R ) )
29 2 eleq2d 
 |-  ( ph -> ( b e. V <-> b e. ( Base ` R ) ) )
30 29 biimpd 
 |-  ( ph -> ( b e. V -> b e. ( Base ` R ) ) )
31 30 adantr 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( b e. V -> b e. ( Base ` R ) ) )
32 31 adantr 
 |-  ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) -> ( b e. V -> b e. ( Base ` R ) ) )
33 32 imp 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> b e. ( Base ` R ) )
34 eqid 
 |-  ( Base ` R ) = ( Base ` R )
35 eqid 
 |-  ( +g ` R ) = ( +g ` R )
36 34 35 ablcom 
 |-  ( ( R e. Abel /\ a e. ( Base ` R ) /\ b e. ( Base ` R ) ) -> ( a ( +g ` R ) b ) = ( b ( +g ` R ) a ) )
37 23 28 33 36 syl3anc 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ( a ( +g ` R ) b ) = ( b ( +g ` R ) a ) )
38 37 fveq2d 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( b ( +g ` R ) a ) ) )
39 simplll 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ph )
40 simpr 
 |-  ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) -> a e. V )
41 40 adantr 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> a e. V )
42 simpr 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> b e. V )
43 3 eqcomd 
 |-  ( ph -> ( +g ` R ) = .+ )
44 43 oveqd 
 |-  ( ph -> ( a ( +g ` R ) b ) = ( a .+ b ) )
45 44 fveq2d 
 |-  ( ph -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( a .+ b ) ) )
46 43 oveqd 
 |-  ( ph -> ( p ( +g ` R ) q ) = ( p .+ q ) )
47 46 fveq2d 
 |-  ( ph -> ( F ` ( p ( +g ` R ) q ) ) = ( F ` ( p .+ q ) ) )
48 45 47 eqeq12d 
 |-  ( ph -> ( ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) <-> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
49 48 3ad2ant1 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) <-> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )
50 5 49 sylibrd 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a ( +g ` R ) b ) ) = ( F ` ( p ( +g ` R ) q ) ) ) )
51 eqid 
 |-  ( +g ` U ) = ( +g ` U )
52 4 50 1 2 6 35 51 imasaddval 
 |-  ( ( ph /\ a e. V /\ b e. V ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( F ` ( a ( +g ` R ) b ) ) )
53 39 41 42 52 syl3anc 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( F ` ( a ( +g ` R ) b ) ) )
54 4 50 1 2 6 35 51 imasaddval 
 |-  ( ( ph /\ b e. V /\ a e. V ) -> ( ( F ` b ) ( +g ` U ) ( F ` a ) ) = ( F ` ( b ( +g ` R ) a ) ) )
55 39 42 41 54 syl3anc 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ( ( F ` b ) ( +g ` U ) ( F ` a ) ) = ( F ` ( b ( +g ` R ) a ) ) )
56 38 53 55 3eqtr4d 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( ( F ` b ) ( +g ` U ) ( F ` a ) ) )
57 56 adantr 
 |-  ( ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) /\ ( ( F ` b ) = y /\ ( F ` a ) = x ) ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( ( F ` b ) ( +g ` U ) ( F ` a ) ) )
58 oveq12 
 |-  ( ( ( F ` a ) = x /\ ( F ` b ) = y ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( x ( +g ` U ) y ) )
59 58 ancoms 
 |-  ( ( ( F ` b ) = y /\ ( F ` a ) = x ) -> ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( x ( +g ` U ) y ) )
60 oveq12 
 |-  ( ( ( F ` b ) = y /\ ( F ` a ) = x ) -> ( ( F ` b ) ( +g ` U ) ( F ` a ) ) = ( y ( +g ` U ) x ) )
61 59 60 eqeq12d 
 |-  ( ( ( F ` b ) = y /\ ( F ` a ) = x ) -> ( ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( ( F ` b ) ( +g ` U ) ( F ` a ) ) <-> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) )
62 61 adantl 
 |-  ( ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) /\ ( ( F ` b ) = y /\ ( F ` a ) = x ) ) -> ( ( ( F ` a ) ( +g ` U ) ( F ` b ) ) = ( ( F ` b ) ( +g ` U ) ( F ` a ) ) <-> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) )
63 57 62 mpbid 
 |-  ( ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) /\ ( ( F ` b ) = y /\ ( F ` a ) = x ) ) -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) )
64 63 exp32 
 |-  ( ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) /\ b e. V ) -> ( ( F ` b ) = y -> ( ( F ` a ) = x -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) ) )
65 64 rexlimdva 
 |-  ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) -> ( E. b e. V ( F ` b ) = y -> ( ( F ` a ) = x -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) ) )
66 65 com23 
 |-  ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ a e. V ) -> ( ( F ` a ) = x -> ( E. b e. V ( F ` b ) = y -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) ) )
67 66 rexlimdva 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( E. a e. V ( F ` a ) = x -> ( E. b e. V ( F ` b ) = y -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) ) )
68 67 impd 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( ( E. a e. V ( F ` a ) = x /\ E. b e. V ( F ` b ) = y ) -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) )
69 22 68 syld 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( ( x e. B /\ y e. B ) -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) )
70 15 69 sylbid 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) )
71 70 imp 
 |-  ( ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) /\ ( x e. ( Base ` U ) /\ y e. ( Base ` U ) ) ) -> ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) )
72 71 ralrimivva 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) )
73 simpr 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) )
74 72 73 jca 
 |-  ( ( ph /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) -> ( A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) )
75 9 74 mpdan 
 |-  ( ph -> ( A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) )
76 eqid 
 |-  ( Base ` U ) = ( Base ` U )
77 76 51 isabl2 
 |-  ( U e. Abel <-> ( U e. Grp /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) )
78 77 anbi1i 
 |-  ( ( U e. Abel /\ ( F ` .0. ) = ( 0g ` U ) ) <-> ( ( U e. Grp /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) /\ ( F ` .0. ) = ( 0g ` U ) ) )
79 an21 
 |-  ( ( ( U e. Grp /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) ) /\ ( F ` .0. ) = ( 0g ` U ) ) <-> ( A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) )
80 78 79 bitri 
 |-  ( ( U e. Abel /\ ( F ` .0. ) = ( 0g ` U ) ) <-> ( A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( x ( +g ` U ) y ) = ( y ( +g ` U ) x ) /\ ( U e. Grp /\ ( F ` .0. ) = ( 0g ` U ) ) ) )
81 75 80 sylibr 
 |-  ( ph -> ( U e. Abel /\ ( F ` .0. ) = ( 0g ` U ) ) )