This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ghomdiv

Description: Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses ghomdiv.1 
|- X = ran G
ghomdiv.2 
|- D = ( /g ` G )
ghomdiv.3 
|- C = ( /g ` H )
Assertion ghomdiv 
|- ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A D B ) ) = ( ( F ` A ) C ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 ghomdiv.1 
 |-  X = ran G
2 ghomdiv.2 
 |-  D = ( /g ` G )
3 ghomdiv.3 
 |-  C = ( /g ` H )
4 simpl2 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> H e. GrpOp )
5 eqid 
 |-  ran H = ran H
6 1 5 ghomf 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F : X --> ran H )
7 6 ffvelcdmda 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ A e. X ) -> ( F ` A ) e. ran H )
8 7 adantrr 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` A ) e. ran H )
9 6 ffvelcdmda 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ B e. X ) -> ( F ` B ) e. ran H )
10 9 adantrl 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` B ) e. ran H )
11 5 3 grponpcan 
 |-  ( ( H e. GrpOp /\ ( F ` A ) e. ran H /\ ( F ` B ) e. ran H ) -> ( ( ( F ` A ) C ( F ` B ) ) H ( F ` B ) ) = ( F ` A ) )
12 4 8 10 11 syl3anc 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( F ` A ) C ( F ` B ) ) H ( F ` B ) ) = ( F ` A ) )
13 1 2 grponpcan 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( ( A D B ) G B ) = A )
14 13 3expb 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) G B ) = A )
15 14 3ad2antl1 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) G B ) = A )
16 15 fveq2d 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( ( A D B ) G B ) ) = ( F ` A ) )
17 1 2 grpodivcl 
 |-  ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) e. X )
18 17 3expb 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( A D B ) e. X )
19 simprr 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> B e. X )
20 18 19 jca 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) e. X /\ B e. X ) )
21 20 3ad2antl1 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( A D B ) e. X /\ B e. X ) )
22 1 ghomlinOLD 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( ( A D B ) e. X /\ B e. X ) ) -> ( ( F ` ( A D B ) ) H ( F ` B ) ) = ( F ` ( ( A D B ) G B ) ) )
23 22 eqcomd 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( ( A D B ) e. X /\ B e. X ) ) -> ( F ` ( ( A D B ) G B ) ) = ( ( F ` ( A D B ) ) H ( F ` B ) ) )
24 21 23 syldan 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( ( A D B ) G B ) ) = ( ( F ` ( A D B ) ) H ( F ` B ) ) )
25 12 16 24 3eqtr2rd 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` ( A D B ) ) H ( F ` B ) ) = ( ( ( F ` A ) C ( F ` B ) ) H ( F ` B ) ) )
26 18 3ad2antl1 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) e. X )
27 6 ffvelcdmda 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A D B ) e. X ) -> ( F ` ( A D B ) ) e. ran H )
28 26 27 syldan 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A D B ) ) e. ran H )
29 5 3 grpodivcl 
 |-  ( ( H e. GrpOp /\ ( F ` A ) e. ran H /\ ( F ` B ) e. ran H ) -> ( ( F ` A ) C ( F ` B ) ) e. ran H )
30 4 8 10 29 syl3anc 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) C ( F ` B ) ) e. ran H )
31 5 grporcan 
 |-  ( ( H e. GrpOp /\ ( ( F ` ( A D B ) ) e. ran H /\ ( ( F ` A ) C ( F ` B ) ) e. ran H /\ ( F ` B ) e. ran H ) ) -> ( ( ( F ` ( A D B ) ) H ( F ` B ) ) = ( ( ( F ` A ) C ( F ` B ) ) H ( F ` B ) ) <-> ( F ` ( A D B ) ) = ( ( F ` A ) C ( F ` B ) ) ) )
32 4 28 30 10 31 syl13anc 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( ( F ` ( A D B ) ) H ( F ` B ) ) = ( ( ( F ` A ) C ( F ` B ) ) H ( F ` B ) ) <-> ( F ` ( A D B ) ) = ( ( F ` A ) C ( F ` B ) ) ) )
33 25 32 mpbid 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A D B ) ) = ( ( F ` A ) C ( F ` B ) ) )