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 | |- A = ( AbsVal ` R ) |
|
| abvtriv.b | |- B = ( Base ` R ) |
||
| abvtriv.z | |- .0. = ( 0g ` R ) |
||
| abvtriv.f | |- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) ) |
||
| Assertion | abvtrivg | |- ( R e. Domn -> F e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | abvtriv.a | |- A = ( AbsVal ` R ) |
|
| 2 | abvtriv.b | |- B = ( Base ` R ) |
|
| 3 | abvtriv.z | |- .0. = ( 0g ` R ) |
|
| 4 | abvtriv.f | |- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) ) |
|
| 5 | eqid | |- ( .r ` R ) = ( .r ` R ) |
|
| 6 | domnring | |- ( R e. Domn -> R e. Ring ) |
|
| 7 | 2 5 3 | domnmuln0 | |- ( ( R e. Domn /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` R ) z ) =/= .0. ) |
| 8 | 1 2 3 4 5 6 7 | abvtrivd | |- ( R e. Domn -> F e. A ) |