Metamath Proof Explorer

Theorem ghminv

Description: A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypotheses ghminv.b 
|- B = ( Base ` S )
ghminv.y 
|- M = ( invg ` S )
ghminv.z 
|- N = ( invg ` T )
Assertion ghminv 
|- ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( M ` X ) ) = ( N ` ( F ` X ) ) )

Proof

Step Hyp Ref Expression
1 ghminv.b 
 |-  B = ( Base ` S )
2 ghminv.y 
 |-  M = ( invg ` S )
3 ghminv.z 
 |-  N = ( invg ` T )
4 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
5 eqid 
 |-  ( +g ` S ) = ( +g ` S )
6 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
7 1 5 6 2 grprinv 
 |-  ( ( S e. Grp /\ X e. B ) -> ( X ( +g ` S ) ( M ` X ) ) = ( 0g ` S ) )
8 4 7 sylan 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( X ( +g ` S ) ( M ` X ) ) = ( 0g ` S ) )
9 8 fveq2d 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( X ( +g ` S ) ( M ` X ) ) ) = ( F ` ( 0g ` S ) ) )
10 1 2 grpinvcl 
 |-  ( ( S e. Grp /\ X e. B ) -> ( M ` X ) e. B )
11 4 10 sylan 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( M ` X ) e. B )
12 eqid 
 |-  ( +g ` T ) = ( +g ` T )
13 1 5 12 ghmlin 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B /\ ( M ` X ) e. B ) -> ( F ` ( X ( +g ` S ) ( M ` X ) ) ) = ( ( F ` X ) ( +g ` T ) ( F ` ( M ` X ) ) ) )
14 11 13 mpd3an3 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( X ( +g ` S ) ( M ` X ) ) ) = ( ( F ` X ) ( +g ` T ) ( F ` ( M ` X ) ) ) )
15 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
16 6 15 ghmid 
 |-  ( F e. ( S GrpHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
17 16 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
18 9 14 17 3eqtr3d 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( ( F ` X ) ( +g ` T ) ( F ` ( M ` X ) ) ) = ( 0g ` T ) )
19 ghmgrp2 
 |-  ( F e. ( S GrpHom T ) -> T e. Grp )
20 19 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> T e. Grp )
21 eqid 
 |-  ( Base ` T ) = ( Base ` T )
22 1 21 ghmf 
 |-  ( F e. ( S GrpHom T ) -> F : B --> ( Base ` T ) )
23 22 ffvelrnda 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` X ) e. ( Base ` T ) )
24 22 adantr 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> F : B --> ( Base ` T ) )
25 24 11 ffvelrnd 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( M ` X ) ) e. ( Base ` T ) )
26 21 12 15 3 grpinvid1 
 |-  ( ( T e. Grp /\ ( F ` X ) e. ( Base ` T ) /\ ( F ` ( M ` X ) ) e. ( Base ` T ) ) -> ( ( N ` ( F ` X ) ) = ( F ` ( M ` X ) ) <-> ( ( F ` X ) ( +g ` T ) ( F ` ( M ` X ) ) ) = ( 0g ` T ) ) )
27 20 23 25 26 syl3anc 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( ( N ` ( F ` X ) ) = ( F ` ( M ` X ) ) <-> ( ( F ` X ) ( +g ` T ) ( F ` ( M ` X ) ) ) = ( 0g ` T ) ) )
28 18 27 mpbird 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( N ` ( F ` X ) ) = ( F ` ( M ` X ) ) )
29 28 eqcomd 
 |-  ( ( F e. ( S GrpHom T ) /\ X e. B ) -> ( F ` ( M ` X ) ) = ( N ` ( F ` X ) ) )