Metamath Proof Explorer

Theorem domnmuln0

Description: In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses domneq0.b 
|- B = ( Base ` R )
domneq0.t 
|- .x. = ( .r ` R )
domneq0.z 
|- .0. = ( 0g ` R )
Assertion domnmuln0 
|- ( ( R e. Domn /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )

Proof

Step Hyp Ref Expression
1 domneq0.b 
 |-  B = ( Base ` R )
2 domneq0.t 
 |-  .x. = ( .r ` R )
3 domneq0.z 
 |-  .0. = ( 0g ` R )
4 an4 
 |-  ( ( ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) <-> ( ( X e. B /\ Y e. B ) /\ ( X =/= .0. /\ Y =/= .0. ) ) )
5 neanior 
 |-  ( ( X =/= .0. /\ Y =/= .0. ) <-> -. ( X = .0. \/ Y = .0. ) )
6 1 2 3 domneq0 
 |-  ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
7 6 3expb 
 |-  ( ( R e. Domn /\ ( X e. B /\ Y e. B ) ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
8 7 necon3abid 
 |-  ( ( R e. Domn /\ ( X e. B /\ Y e. B ) ) -> ( ( X .x. Y ) =/= .0. <-> -. ( X = .0. \/ Y = .0. ) ) )
9 5 8 bitr4id 
 |-  ( ( R e. Domn /\ ( X e. B /\ Y e. B ) ) -> ( ( X =/= .0. /\ Y =/= .0. ) <-> ( X .x. Y ) =/= .0. ) )
10 9 biimpd 
 |-  ( ( R e. Domn /\ ( X e. B /\ Y e. B ) ) -> ( ( X =/= .0. /\ Y =/= .0. ) -> ( X .x. Y ) =/= .0. ) )
11 10 expimpd 
 |-  ( R e. Domn -> ( ( ( X e. B /\ Y e. B ) /\ ( X =/= .0. /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. ) )
12 4 11 biimtrid 
 |-  ( R e. Domn -> ( ( ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. ) )
13 12 3impib 
 |-  ( ( R e. Domn /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )