Description: The trivial absolute value. This theorem is not true for rings with zero divisors, which violate the multiplication axiom; abvdom is the converse of this theorem. (Contributed by SN, 25-Jun-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | abvtriv.a | ⊢ 𝐴 = ( AbsVal ‘ 𝑅 ) | |
| abvtriv.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | ||
| abvtriv.z | ⊢ 0 = ( 0g ‘ 𝑅 ) | ||
| abvtriv.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) ) | ||
| Assertion | abvtrivg | ⊢ ( 𝑅 ∈ Domn → 𝐹 ∈ 𝐴 ) |
| 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 | domnring | ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring ) | |
| 7 | 2 5 3 | domnmuln0 | ⊢ ( ( 𝑅 ∈ Domn ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ≠ 0 ) |
| 8 | 1 2 3 4 5 6 7 | abvtrivd | ⊢ ( 𝑅 ∈ Domn → 𝐹 ∈ 𝐴 ) |