Metamath Proof Explorer

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 → 𝐹𝐴 )