dvdsrcl2

Description: Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014)

	Ref	Expression
Hypotheses	dvdsr.1	$⊢ B = {Base}_{R}$
	dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
Assertion	dvdsrcl2	$⊢ (R \in Ring \land X \underset{˙}{∥} Y) \to Y \in B$

Step	Hyp	Ref	Expression
1		dvdsr.1	$⊢ B = {Base}_{R}$
2		dvdsr.2	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		eqid	$⊢ \cdot_{R} = \cdot_{R}$
4	1 2 3	dvdsr	$⊢ X \underset{˙}{∥} Y \leftrightarrow (X \in B \land \exists x \in B x \cdot_{R} X = Y)$
5	1 3	ringcl	$⊢ (R \in Ring \land x \in B \land X \in B) \to x \cdot_{R} X \in B$
6	5	3expa	$⊢ ((R \in Ring \land x \in B) \land X \in B) \to x \cdot_{R} X \in B$
7	6	an32s	$⊢ ((R \in Ring \land X \in B) \land x \in B) \to x \cdot_{R} X \in B$
8		eleq1	$⊢ x \cdot_{R} X = Y \to (x \cdot_{R} X \in B \leftrightarrow Y \in B)$
9	7 8	syl5ibcom	$⊢ ((R \in Ring \land X \in B) \land x \in B) \to (x \cdot_{R} X = Y \to Y \in B)$
10	9	rexlimdva	$⊢ (R \in Ring \land X \in B) \to (\exists x \in B x \cdot_{R} X = Y \to Y \in B)$
11	10	impr	$⊢ (R \in Ring \land (X \in B \land \exists x \in B x \cdot_{R} X = Y)) \to Y \in B$
12	4 11	sylan2b	$⊢ (R \in Ring \land X \underset{˙}{∥} Y) \to Y \in B$

Metamath Proof Explorer