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

Metamath Proof Explorer

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. ) )