Description: A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014)
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 | drngmulne0 | |- ( ph -> ( ( X .x. Y ) =/= .0. <-> ( X =/= .0. /\ Y =/= .0. ) ) ) |
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 | 1 2 3 4 5 6 | drngmul0or | |- ( ph -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) ) |
8 | 7 | necon3abid | |- ( ph -> ( ( X .x. Y ) =/= .0. <-> -. ( X = .0. \/ Y = .0. ) ) ) |
9 | neanior | |- ( ( X =/= .0. /\ Y =/= .0. ) <-> -. ( X = .0. \/ Y = .0. ) ) |
|
10 | 8 9 | bitr4di | |- ( ph -> ( ( X .x. Y ) =/= .0. <-> ( X =/= .0. /\ Y =/= .0. ) ) ) |