Metamath Proof Explorer

Theorem subrgmcl

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

		Ref	Expression
	Hypothesis	subrgmcl.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	Assertion	subrgmcl	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to X \underset{˙}{\cdot} Y \in A$

Proof

Step	Hyp	Ref	Expression
1		subrgmcl.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
2		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
3	2	subrgring	$⊢ A \in SubRing (R) \to R ↾_{𝑠} A \in Ring$
4	3	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to R ↾_{𝑠} A \in Ring$
5		simp2	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to X \in A$
6	2	subrgbas	$⊢ A \in SubRing (R) \to A = {Base}_{(R ↾_{𝑠} A)}$
7	6	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to A = {Base}_{(R ↾_{𝑠} A)}$
8	5 7	eleqtrd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to X \in {Base}_{(R ↾_{𝑠} A)}$
9		simp3	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to Y \in A$
10	9 7	eleqtrd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to Y \in {Base}_{(R ↾_{𝑠} A)}$
11		eqid	$⊢ {Base}_{(R ↾_{𝑠} A)} = {Base}_{(R ↾_{𝑠} A)}$
12		eqid	$⊢ \cdot_{(R ↾_{𝑠} A)} = \cdot_{(R ↾_{𝑠} A)}$
13	11 12	ringcl	$⊢ (R ↾_{𝑠} A \in Ring \land X \in {Base}_{(R ↾_{𝑠} A)} \land Y \in {Base}_{(R ↾_{𝑠} A)}) \to X \cdot_{(R ↾_{𝑠} A)} Y \in {Base}_{(R ↾_{𝑠} A)}$
14	4 8 10 13	syl3anc	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to X \cdot_{(R ↾_{𝑠} A)} Y \in {Base}_{(R ↾_{𝑠} A)}$
15	2 1	ressmulr	$⊢ A \in SubRing (R) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
16	15	3ad2ant1	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
17	16	oveqd	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to X \underset{˙}{\cdot} Y = X \cdot_{(R ↾_{𝑠} A)} Y$
18	14 17 7	3eltr4d	$⊢ (A \in SubRing (R) \land X \in A \land Y \in A) \to X \underset{˙}{\cdot} Y \in A$