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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
domneq0.t ⊢ · = ( .r ‘ 𝑅 )
domneq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion domnmuln0 ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 domneq0.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 domneq0.t ⊢ · = ( .r ‘ 𝑅 )
3 domneq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 an4 ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) ↔ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )
5 neanior ⊢ ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) )
6 1 2 3 domneq0 ⊢ ( ( 𝑅 ∈ Domn ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
7 6 3expb ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
8 7 necon3abid ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
9 5 8 bitr4id ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ↔ ( 𝑋 · 𝑌 ) ≠ 0 ) )
10 9 biimpd ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) → ( 𝑋 · 𝑌 ) ≠ 0 ) )
11 10 expimpd ⊢ ( 𝑅 ∈ Domn → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 ) )
12 4 11 biimtrid ⊢ ( 𝑅 ∈ Domn → ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 ) )
13 12 3impib ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑌 ≠ 0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )