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 ⊢ 𝐵 = ( Base ‘ 𝑆 )
ghminv.y ⊢ 𝑀 = ( invg ‘ 𝑆 )
ghminv.z ⊢ 𝑁 = ( invg ‘ 𝑇 )
Assertion ghminv ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 ghminv.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 ghminv.y ⊢ 𝑀 = ( invg ‘ 𝑆 )
3 ghminv.z ⊢ 𝑁 = ( invg ‘ 𝑇 )
4 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
5 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
6 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
7 1 5 6 2 grprinv ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑆 ) ( 𝑀 ‘ 𝑋 ) ) = ( 0g ‘ 𝑆 ) )
8 4 7 sylan ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( +g ‘ 𝑆 ) ( 𝑀 ‘ 𝑋 ) ) = ( 0g ‘ 𝑆 ) )
9 8 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ( +g ‘ 𝑆 ) ( 𝑀 ‘ 𝑋 ) ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) )
10 1 2 grpinvcl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝐵 )
11 4 10 sylan ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) ∈ 𝐵 )
12 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
13 1 5 12 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑋 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ( +g ‘ 𝑆 ) ( 𝑀 ‘ 𝑋 ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
14 11 13 mpd3an3 ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ( +g ‘ 𝑆 ) ( 𝑀 ‘ 𝑋 ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ) )
15 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
16 6 15 ghmid ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
17 16 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
18 9 14 17 3eqtr3d ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑇 ) )
19 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑇 ∈ Grp )
20 19 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑇 ∈ Grp )
21 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
22 1 21 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
23 22 ffvelcdmda ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
24 22 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
25 24 11 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑇 ) )
26 21 12 15 3 grpinvid1 ⊢ ( ( 𝑇 ∈ Grp ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) ∧ ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ∈ ( Base ‘ 𝑇 ) ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑇 ) ) )
27 20 23 25 26 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) ) = ( 0g ‘ 𝑇 ) ) )
28 18 27 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) )
29 28 eqcomd ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑀 ‘ 𝑋 ) ) = ( 𝑁 ‘ ( 𝐹 ‘ 𝑋 ) ) )