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

Metamath Proof Explorer

Theorem dvdsr01

Description: In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg .) (Contributed by Stefan O'Rear, 29-Mar-2015)

		Ref	Expression
	Hypotheses	dvdsr0.b	$⊢ B = {Base}_{R}$
		dvdsr0.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
		dvdsr0.z	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	dvdsr01	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		dvdsr0.b	$⊢ B = {Base}_{R}$
2		dvdsr0.d	$⊢ \underset{˙}{∥} = ∥_{r} (R)$
3		dvdsr0.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1 3	ring0cl	$⊢ R \in Ring \to \underset{˙}{0} \in B$
5		eqid	$⊢ \cdot_{R} = \cdot_{R}$
6	1 5 3	ringlz	$⊢ (R \in Ring \land X \in B) \to \underset{˙}{0} \cdot_{R} X = \underset{˙}{0}$
7		oveq1	$⊢ x = \underset{˙}{0} \to x \cdot_{R} X = \underset{˙}{0} \cdot_{R} X$
8	7	eqeq1d	$⊢ x = \underset{˙}{0} \to (x \cdot_{R} X = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \cdot_{R} X = \underset{˙}{0})$
9	8	rspcev	$⊢ (\underset{˙}{0} \in B \land \underset{˙}{0} \cdot_{R} X = \underset{˙}{0}) \to \exists x \in B x \cdot_{R} X = \underset{˙}{0}$
10	4 6 9	syl2an2r	$⊢ (R \in Ring \land X \in B) \to \exists x \in B x \cdot_{R} X = \underset{˙}{0}$
11	1 2 5	dvdsr2	$⊢ X \in B \to (X \underset{˙}{∥} \underset{˙}{0} \leftrightarrow \exists x \in B x \cdot_{R} X = \underset{˙}{0})$
12	11	adantl	$⊢ (R \in Ring \land X \in B) \to (X \underset{˙}{∥} \underset{˙}{0} \leftrightarrow \exists x \in B x \cdot_{R} X = \underset{˙}{0})$
13	10 12	mpbird	$⊢ (R \in Ring \land X \in B) \to X \underset{˙}{∥} \underset{˙}{0}$