Metamath Proof Explorer

Theorem subrngmcl

Description: A subring is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014) Generalization of subrgmcl . (Revised by AV, 14-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		subrngmcl.p	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
2		eqid	$⊢ R ↾_{𝑠} A = R ↾_{𝑠} A$
3	2	subrngrng	$⊢ A \in SubRng (R) \to R ↾_{𝑠} A \in Rng$
4	3	3ad2ant1	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to R ↾_{𝑠} A \in Rng$
5		simp2	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to X \in A$
6	2	subrngbas	$⊢ A \in SubRng (R) \to A = {Base}_{(R ↾_{𝑠} A)}$
7	6	3ad2ant1	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to A = {Base}_{(R ↾_{𝑠} A)}$
8	5 7	eleqtrd	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to X \in {Base}_{(R ↾_{𝑠} A)}$
9		simp3	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to Y \in A$
10	9 7	eleqtrd	$⊢ (A \in SubRng (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	rngcl	$⊢ (R ↾_{𝑠} A \in Rng \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 SubRng (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 SubRng (R) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
16	15	3ad2ant1	$⊢ (A \in SubRng (R) \land X \in A \land Y \in A) \to \underset{˙}{\cdot} = \cdot_{(R ↾_{𝑠} A)}$
17	16	oveqd	$⊢ (A \in SubRng (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 SubRng (R) \land X \in A \land Y \in A) \to X \underset{˙}{\cdot} Y \in A$