Theorem drngmul0or

Description: A product is zero iff one of its factors is zero. (Contributed by NM, 8-Oct-2014) (Proof shortened by SN, 25-Jun-2025)

	Ref	Expression
Hypotheses	drngmuleq0.b	|- B = ( Base ` R )
	drngmuleq0.o	|- .0. = ( 0g ` R )
	drngmuleq0.t	|- .x. = ( .r ` R )
	drngmuleq0.r	|- ( ph -> R e. DivRing )
	drngmuleq0.x	|- ( ph -> X e. B )
	drngmuleq0.y	|- ( ph -> Y e. B )
Assertion	drngmul0or	|- ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		drngmuleq0.b	|- B = ( Base ` R )
2		drngmuleq0.o	|- .0. = ( 0g ` R )
3		drngmuleq0.t	|- .x. = ( .r ` R )
4		drngmuleq0.r	|- ( ph -> R e. DivRing )
5		drngmuleq0.x	|- ( ph -> X e. B )
6		drngmuleq0.y	|- ( ph -> Y e. B )
7		drngdomn	|- ( R e. DivRing -> R e. Domn )
8	4 7	syl	|- ( ph -> R e. Domn )
9	1 3 2	domneq0	|- ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
10	8 5 6 9	syl3anc	|- ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )