Theorem subrgmcl

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

	Ref	Expression
Hypothesis	subrgmcl.p	|- .x. = ( .r ` R )
Assertion	subrgmcl	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )

Proof

Step	Hyp	Ref	Expression
1		subrgmcl.p	|- .x. = ( .r ` R )
2		eqid	|- ( R |`s A ) = ( R |`s A )
3	2	subrgring	|- ( A e. ( SubRing ` R ) -> ( R |`s A ) e. Ring )
4	3	3ad2ant1	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( R |`s A ) e. Ring )
5		simp2	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> X e. A )
6	2	subrgbas	|- ( A e. ( SubRing ` R ) -> A = ( Base ` ( R |`s A ) ) )
7	6	3ad2ant1	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> A = ( Base ` ( R |`s A ) ) )
8	5 7	eleqtrd	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> X e. ( Base ` ( R |`s A ) ) )
9		simp3	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> Y e. A )
10	9 7	eleqtrd	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> Y e. ( Base ` ( R |`s A ) ) )
11		eqid	|- ( Base ` ( R |`s A ) ) = ( Base ` ( R |`s A ) )
12		eqid	|- ( .r ` ( R |`s A ) ) = ( .r ` ( R |`s A ) )
13	11 12	ringcl	|- ( ( ( R |`s A ) e. Ring /\ X e. ( Base ` ( R |`s A ) ) /\ Y e. ( Base ` ( R |`s A ) ) ) -> ( X ( .r ` ( R |`s A ) ) Y ) e. ( Base ` ( R |`s A ) ) )
14	4 8 10 13	syl3anc	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X ( .r ` ( R |`s A ) ) Y ) e. ( Base ` ( R |`s A ) ) )
15	2 1	ressmulr	|- ( A e. ( SubRing ` R ) -> .x. = ( .r ` ( R |`s A ) ) )
16	15	3ad2ant1	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> .x. = ( .r ` ( R |`s A ) ) )
17	16	oveqd	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) = ( X ( .r ` ( R |`s A ) ) Y ) )
18	14 17 7	3eltr4d	|- ( ( A e. ( SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )