Theorem subgcl

Description: A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypothesis	subgcl.p	⊢ + = ( +g ‘ 𝐺 )
Assertion	subgcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		subgcl.p	⊢ + = ( +g ‘ 𝐺 )
2		eqid	⊢ ( 𝐺 ↾s 𝑆 ) = ( 𝐺 ↾s 𝑆 )
3	2	subggrp	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
4	3	3ad2ant1	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝐺 ↾s 𝑆 ) ∈ Grp )
5		simp2	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
6	2	subgbas	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
7	6	3ad2ant1	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑆 = ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
8	5 7	eleqtrd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
9		simp3	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ 𝑆 )
10	9 7	eleqtrd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
11		eqid	⊢ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑆 ) )
12		eqid	⊢ ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) = ( +g ‘ ( 𝐺 ↾s 𝑆 ) )
13	11 12	grpcl	⊢ ( ( ( 𝐺 ↾s 𝑆 ) ∈ Grp ∧ 𝑋 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ∧ 𝑌 ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) ) → ( 𝑋 ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) 𝑌 ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
14	4 8 10 13	syl3anc	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) 𝑌 ) ∈ ( Base ‘ ( 𝐺 ↾s 𝑆 ) ) )
15	2 1	ressplusg	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → + = ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) )
16	15	3ad2ant1	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → + = ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) )
17	16	oveqd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) = ( 𝑋 ( +g ‘ ( 𝐺 ↾s 𝑆 ) ) 𝑌 ) )
18	14 17 7	3eltr4d	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )