Theorem subgcl

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

	Ref	Expression
Hypothesis	subgcl.p	|- .+ = ( +g ` G )
Assertion	subgcl	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )

Proof

Step	Hyp	Ref	Expression
1		subgcl.p	|- .+ = ( +g ` G )
2		eqid	|- ( G |`s S ) = ( G |`s S )
3	2	subggrp	|- ( S e. ( SubGrp ` G ) -> ( G |`s S ) e. Grp )
4	3	3ad2ant1	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( G |`s S ) e. Grp )
5		simp2	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. S )
6	2	subgbas	|- ( S e. ( SubGrp ` G ) -> S = ( Base ` ( G |`s S ) ) )
7	6	3ad2ant1	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> S = ( Base ` ( G |`s S ) ) )
8	5 7	eleqtrd	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> X e. ( Base ` ( G |`s S ) ) )
9		simp3	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. S )
10	9 7	eleqtrd	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> Y e. ( Base ` ( G |`s S ) ) )
11		eqid	|- ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) )
12		eqid	|- ( +g ` ( G |`s S ) ) = ( +g ` ( G |`s S ) )
13	11 12	grpcl	|- ( ( ( G |`s S ) e. Grp /\ X e. ( Base ` ( G |`s S ) ) /\ Y e. ( Base ` ( G |`s S ) ) ) -> ( X ( +g ` ( G |`s S ) ) Y ) e. ( Base ` ( G |`s S ) ) )
14	4 8 10 13	syl3anc	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X ( +g ` ( G |`s S ) ) Y ) e. ( Base ` ( G |`s S ) ) )
15	2 1	ressplusg	|- ( S e. ( SubGrp ` G ) -> .+ = ( +g ` ( G |`s S ) ) )
16	15	3ad2ant1	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> .+ = ( +g ` ( G |`s S ) ) )
17	16	oveqd	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) = ( X ( +g ` ( G |`s S ) ) Y ) )
18	14 17 7	3eltr4d	|- ( ( S e. ( SubGrp ` G ) /\ X e. S /\ Y e. S ) -> ( X .+ Y ) e. S )