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

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 ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑋 ) = ( 𝐽 ‘ 𝑋 ) )