Metamath Proof Explorer

Theorem abvn0b

Description: Another characterization of domains, hinted at in abvtrivg : a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypothesis abvn0b.b ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
Assertion abvn0b ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 abvn0b.b ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 domnnzr ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ NzRing )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) )
6 1 3 4 5 abvtrivg ⊢ ( 𝑅 ∈ Domn → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) ) ∈ 𝐴 )
7 6 ne0d ⊢ ( 𝑅 ∈ Domn → 𝐴 ≠ ∅ )
8 2 7 jca ⊢ ( 𝑅 ∈ Domn → ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) )
9 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
10 neanior ⊢ ( ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ↔ ¬ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) )
11 an4 ⊢ ( ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) ↔ ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 1 3 4 12 abvdom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) )
14 13 3expib ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
15 11 14 biimtrid ⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
16 15 expdimp ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
17 10 16 biimtrrid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ¬ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
18 17 necon4bd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
19 18 ralrimivva ⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
20 19 exlimiv ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
21 9 20 sylbi ⊢ ( 𝐴 ≠ ∅ → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
22 21 anim2i ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) ) )
23 3 12 4 isdomn ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) ) )
24 22 23 sylibr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) → 𝑅 ∈ Domn )
25 8 24 impbii ⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) )