Metamath Proof Explorer


Theorem subginv

Description: The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses subg0.h 𝐻 = ( 𝐺s 𝑆 )
subginv.i 𝐼 = ( invg𝐺 )
subginv.j 𝐽 = ( invg𝐻 )
Assertion subginv ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝐼𝑋 ) = ( 𝐽𝑋 ) )

Proof

Step Hyp Ref Expression
1 subg0.h 𝐻 = ( 𝐺s 𝑆 )
2 subginv.i 𝐼 = ( invg𝐺 )
3 subginv.j 𝐽 = ( invg𝐻 )
4 1 subggrp ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
5 1 subgbas ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
6 5 eleq2d ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋𝑆𝑋 ∈ ( Base ‘ 𝐻 ) ) )
7 6 biimpa ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
8 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
9 eqid ( +g𝐻 ) = ( +g𝐻 )
10 eqid ( 0g𝐻 ) = ( 0g𝐻 )
11 8 9 10 3 grprinv ( ( 𝐻 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑋 ( +g𝐻 ) ( 𝐽𝑋 ) ) = ( 0g𝐻 ) )
12 4 7 11 syl2an2r ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝑋 ( +g𝐻 ) ( 𝐽𝑋 ) ) = ( 0g𝐻 ) )
13 eqid ( +g𝐺 ) = ( +g𝐺 )
14 1 13 ressplusg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g𝐺 ) = ( +g𝐻 ) )
15 14 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( +g𝐺 ) = ( +g𝐻 ) )
16 15 oveqd ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝑋 ( +g𝐺 ) ( 𝐽𝑋 ) ) = ( 𝑋 ( +g𝐻 ) ( 𝐽𝑋 ) ) )
17 eqid ( 0g𝐺 ) = ( 0g𝐺 )
18 1 17 subg0 ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g𝐺 ) = ( 0g𝐻 ) )
19 18 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 0g𝐺 ) = ( 0g𝐻 ) )
20 12 16 19 3eqtr4d ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝑋 ( +g𝐺 ) ( 𝐽𝑋 ) ) = ( 0g𝐺 ) )
21 subgrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
22 21 adantr ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → 𝐺 ∈ Grp )
23 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
24 23 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
25 24 sselda ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
26 8 3 grpinvcl ( ( 𝐻 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐻 ) )
27 26 ex ( 𝐻 ∈ Grp → ( 𝑋 ∈ ( Base ‘ 𝐻 ) → ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐻 ) ) )
28 4 27 syl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋 ∈ ( Base ‘ 𝐻 ) → ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐻 ) ) )
29 5 eleq2d ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝐽𝑋 ) ∈ 𝑆 ↔ ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐻 ) ) )
30 28 6 29 3imtr4d ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑋𝑆 → ( 𝐽𝑋 ) ∈ 𝑆 ) )
31 30 imp ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝐽𝑋 ) ∈ 𝑆 )
32 24 sselda ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐽𝑋 ) ∈ 𝑆 ) → ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐺 ) )
33 31 32 syldan ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐺 ) )
34 23 13 17 2 grpinvid1 ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐽𝑋 ) ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐼𝑋 ) = ( 𝐽𝑋 ) ↔ ( 𝑋 ( +g𝐺 ) ( 𝐽𝑋 ) ) = ( 0g𝐺 ) ) )
35 22 25 33 34 syl3anc ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( ( 𝐼𝑋 ) = ( 𝐽𝑋 ) ↔ ( 𝑋 ( +g𝐺 ) ( 𝐽𝑋 ) ) = ( 0g𝐺 ) ) )
36 20 35 mpbird ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋𝑆 ) → ( 𝐼𝑋 ) = ( 𝐽𝑋 ) )