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 = inv g ⁡ S
ghminv.z ⊢ N = inv g ⁡ T
Assertion ghminv ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ M ⁡ X = N ⁡ F ⁡ X

Proof

Step Hyp Ref Expression
1 ghminv.b ⊢ B = Base S
2 ghminv.y ⊢ M = inv g ⁡ S
3 ghminv.z ⊢ N = inv g ⁡ T
4 ghmgrp1 ⊢ F ∈ S GrpHom T → S ∈ Grp
5 eqid ⊢ + S = + S
6 eqid ⊢ 0 S = 0 S
7 1 5 6 2 grprinv ⊢ S ∈ Grp ∧ X ∈ B → X + S M ⁡ X = 0 S
8 4 7 sylan ⊢ F ∈ S GrpHom T ∧ X ∈ B → X + S M ⁡ X = 0 S
9 8 fveq2d ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ X + S M ⁡ X = F ⁡ 0 S
10 1 2 grpinvcl ⊢ S ∈ Grp ∧ X ∈ B → M ⁡ X ∈ B
11 4 10 sylan ⊢ F ∈ S GrpHom T ∧ X ∈ B → M ⁡ X ∈ B
12 eqid ⊢ + T = + T
13 1 5 12 ghmlin ⊢ F ∈ S GrpHom T ∧ X ∈ B ∧ M ⁡ X ∈ B → F ⁡ X + S M ⁡ X = F ⁡ X + T F ⁡ M ⁡ X
14 11 13 mpd3an3 ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ X + S M ⁡ X = F ⁡ X + T F ⁡ M ⁡ X
15 eqid ⊢ 0 T = 0 T
16 6 15 ghmid ⊢ F ∈ S GrpHom T → F ⁡ 0 S = 0 T
17 16 adantr ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ 0 S = 0 T
18 9 14 17 3eqtr3d ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ X + T F ⁡ M ⁡ X = 0 T
19 ghmgrp2 ⊢ F ∈ S GrpHom T → T ∈ Grp
20 19 adantr ⊢ F ∈ S GrpHom T ∧ X ∈ B → T ∈ Grp
21 eqid ⊢ Base T = Base T
22 1 21 ghmf ⊢ F ∈ S GrpHom T → F : B ⟶ Base T
23 22 ffvelcdmda ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ X ∈ Base T
24 22 adantr ⊢ F ∈ S GrpHom T ∧ X ∈ B → F : B ⟶ Base T
25 24 11 ffvelcdmd ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ M ⁡ X ∈ Base T
26 21 12 15 3 grpinvid1 ⊢ T ∈ Grp ∧ F ⁡ X ∈ Base T ∧ F ⁡ M ⁡ X ∈ Base T → N ⁡ F ⁡ X = F ⁡ M ⁡ X ↔ F ⁡ X + T F ⁡ M ⁡ X = 0 T
27 20 23 25 26 syl3anc ⊢ F ∈ S GrpHom T ∧ X ∈ B → N ⁡ F ⁡ X = F ⁡ M ⁡ X ↔ F ⁡ X + T F ⁡ M ⁡ X = 0 T
28 18 27 mpbird ⊢ F ∈ S GrpHom T ∧ X ∈ B → N ⁡ F ⁡ X = F ⁡ M ⁡ X
29 28 eqcomd ⊢ F ∈ S GrpHom T ∧ X ∈ B → F ⁡ M ⁡ X = N ⁡ F ⁡ X