This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abvtriv

Description: The trivial absolute value. (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses abvtriv.a ⊢ A = AbsVal ⁡ R
abvtriv.b ⊢ B = Base R
abvtriv.z ⊢ 0 ˙ = 0 R
abvtriv.f ⊢ F = x ∈ B ⟼ if x = 0 ˙ 0 1
Assertion abvtriv ⊢ R ∈ DivRing → F ∈ A

Proof

Step Hyp Ref Expression
1 abvtriv.a ⊢ A = AbsVal ⁡ R
2 abvtriv.b ⊢ B = Base R
3 abvtriv.z ⊢ 0 ˙ = 0 R
4 abvtriv.f ⊢ F = x ∈ B ⟼ if x = 0 ˙ 0 1
5 drngdomn ⊢ R ∈ DivRing → R ∈ Domn
6 1 2 3 4 abvtrivg ⊢ R ∈ Domn → F ∈ A
7 5 6 syl ⊢ R ∈ DivRing → F ∈ A