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

Metamath Proof Explorer

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 )