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

Metamath Proof Explorer

Theorem subginvcl

Description: The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis subginvcl.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion subginvcl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 subginvcl.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
2 eqid ⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
3 2 subggrp ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
4 simpr ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
5 2 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
6 5 adantr ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
7 4 6 eleqtrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
8 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) )
9 eqid ⊢ ( invg ‘ ( 𝐺 ↾s 𝑆 ) ) = ( invg ‘ ( 𝐺 ↾s 𝑆 ) )
10 8 9 grpinvcl ⊢ ( ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ∧ 𝑋 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) → ( ( invg ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
11 3 7 10 syl2an2r ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → ( ( invg ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑋 ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
12 2 1 9 subginv ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑋 ) = ( ( invg ‘ ( 𝐺 ↾s 𝑆 ) ) ‘ 𝑋 ) )
13 11 12 6 3eltr4d ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )