Theorem domnmuln0rd

Description: In a domain, factors of a nonzero product are nonzero. (Contributed by Thierry Arnoux, 8-Jun-2025)

	Ref	Expression
Hypotheses	domnmuln0rd.b	|- B = ( Base ` R )
	domnmuln0rd.t	|- .x. = ( .r ` R )
	domnmuln0rd.z	|- .0. = ( 0g ` R )
	domnmuln0rd.1	|- ( ph -> R e. Domn )
	domnmuln0rd.2	|- ( ph -> X e. B )
	domnmuln0rd.3	|- ( ph -> Y e. B )
	domnmuln0rd.4	|- ( ph -> ( X .x. Y ) =/= .0. )
Assertion	domnmuln0rd	|- ( ph -> ( X =/= .0. /\ Y =/= .0. ) )

Proof

Step	Hyp	Ref	Expression
1		domnmuln0rd.b	|- B = ( Base ` R )
2		domnmuln0rd.t	|- .x. = ( .r ` R )
3		domnmuln0rd.z	|- .0. = ( 0g ` R )
4		domnmuln0rd.1	|- ( ph -> R e. Domn )
5		domnmuln0rd.2	|- ( ph -> X e. B )
6		domnmuln0rd.3	|- ( ph -> Y e. B )
7		domnmuln0rd.4	|- ( ph -> ( X .x. Y ) =/= .0. )
8	1 2 3	domneq0	|- ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
9	4 5 6 8	syl3anc	|- ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
10	9	necon3abid	|- ( ph -> ( ( X .x. Y ) =/= .0. <-> -. ( X = .0. \/ Y = .0. ) ) )
11	7 10	mpbid	|- ( ph -> -. ( X = .0. \/ Y = .0. ) )
12		ioran	|- ( -. ( X = .0. \/ Y = .0. ) <-> ( -. X = .0. /\ -. Y = .0. ) )
13	11 12	sylib	|- ( ph -> ( -. X = .0. /\ -. Y = .0. ) )
14		neqne	|- ( -. X = .0. -> X =/= .0. )
15		neqne	|- ( -. Y = .0. -> Y =/= .0. )
16	14 15	anim12i	|- ( ( -. X = .0. /\ -. Y = .0. ) -> ( X =/= .0. /\ Y =/= .0. ) )
17	13 16	syl	|- ( ph -> ( X =/= .0. /\ Y =/= .0. ) )