Theorem abvtrivg

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=\mathrm{AbsVal}\left(R\right)$$
	abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
	abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
	abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
Assertion	abvtrivg	$$⊢R\in \mathrm{Domn}\to F\in A$$

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
3		abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
5		eqid	$$⊢{\cdot }_R={\cdot }_R$$
6		domnring	$$⊢R\in \mathrm{Domn}\to R\in \mathrm{Ring}$$
7	2 5 3	domnmuln0	$$⊢\left(R\in \mathrm{Domn}\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{R}z\ne \underset{\dot{}}{0}$$
8	1 2 3 4 5 6 7	abvtrivd	$$⊢R\in \mathrm{Domn}\to F\in A$$