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