Theorem abvn0b

Description: Another characterization of domains, hinted at in abvtriv : 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		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7		domnring	⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
8	3 6 4	domnmuln0	⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) )
9	1 3 4 5 6 7 8	abvtrivd	⊢ ( 𝑅 ∈ Domn → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑅 ) , 0 , 1 ) ) ∈ 𝐴 )
10	9	ne0d	⊢ ( 𝑅 ∈ Domn → 𝐴 ≠ ∅ )
11	2 10	jca	⊢ ( 𝑅 ∈ Domn → ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) )
12		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
13		neanior	⊢ ( ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ↔ ¬ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) )
14		an4	⊢ ( ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) ↔ ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) )
15	1 3 4 6	abvdom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) )
16	15	3expib	⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
17	14 16	syl5bi	⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
18	17	expdimp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
19	13 18	syl5bir	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ¬ ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
20	19	necon4bd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
21	20	ralrimivva	⊢ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
22	21	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
23	12 22	sylbi	⊢ ( 𝐴 ≠ ∅ → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) )
24	23	anim2i	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) → ( 𝑅 ∈ NzRing ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) ) )
25	3 6 4	isdomn	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) = ( 0g ‘ 𝑅 ) → ( 𝑦 = ( 0g ‘ 𝑅 ) ∨ 𝑧 = ( 0g ‘ 𝑅 ) ) ) ) )
26	24 25	sylibr	⊢ ( ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) → 𝑅 ∈ Domn )
27	11 26	impbii	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ 𝐴 ≠ ∅ ) )