Theorem abvtriv

Description: The trivial absolute value. (This theorem is true as long as R is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	abvtriv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvtriv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	abvtriv.z	⊢ 0 = ( 0g ‘ 𝑅 )
	abvtriv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
Assertion	abvtriv	⊢ ( 𝑅 ∈ DivRing → 𝐹 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvtriv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abvtriv.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		abvtriv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
7		biid	⊢ ( 𝑅 ∈ DivRing ↔ 𝑅 ∈ DivRing )
8		eldifsn	⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) )
9		eldifsn	⊢ ( 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) )
10	2 5 3	drngmcl	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ ( 𝐵 ∖ { 0 } ) )
11	7 8 9 10	syl3anbr	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ ( 𝐵 ∖ { 0 } ) )
12		eldifsn	⊢ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ 0 ) )
13	11 12	sylib	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ 0 ) )
14	13	simprd	⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ 0 )
15	1 2 3 4 5 6 14	abvtrivd	⊢ ( 𝑅 ∈ DivRing → 𝐹 ∈ 𝐴 )