Metamath Proof Explorer

Theorem abvtrivd

Description: The trivial absolute value. (Contributed 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 ) )
abvtrivd.1 ⊢ · = ( .r ‘ 𝑅 )
abvtrivd.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
abvtrivd.3 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ≠ 0 )
Assertion abvtrivd ( 𝜑 → 𝐹 ∈ 𝐴 )

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 abvtrivd.1 ⊢ · = ( .r ‘ 𝑅 )
6 abvtrivd.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 abvtrivd.3 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ≠ 0 )
8 1 a1i ⊢ ( 𝜑 → 𝐴 = ( AbsVal ‘ 𝑅 ) )
9 2 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
10 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
11 5 a1i ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
12 3 a1i ⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
13 0re ⊢ 0 ∈ ℝ
14 1re ⊢ 1 ∈ ℝ
15 13 14 ifcli ⊢ if ( 𝑥 = 0 , 0 , 1 ) ∈ ℝ
16 15 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 = 0 , 0 , 1 ) ∈ ℝ )
17 16 4 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ℝ )
18 2 3 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
19 iftrue ⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , 0 , 1 ) = 0 )
20 c0ex ⊢ 0 ∈ V
21 19 4 20 fvmpt ⊢ ( 0 ∈ 𝐵 → ( 𝐹 ‘ 0 ) = 0 )
22 6 18 21 3syl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = 0 )
23 0lt1 ⊢ 0 < 1
24 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 0 ↔ 𝑦 = 0 ) )
25 24 ifbid ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑦 = 0 , 0 , 1 ) )
26 1ex ⊢ 1 ∈ V
27 20 26 ifex ⊢ if ( 𝑦 = 0 , 0 , 1 ) ∈ V
28 25 4 27 fvmpt ⊢ ( 𝑦 ∈ 𝐵 → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , 1 ) )
29 ifnefalse ⊢ ( 𝑦 ≠ 0 → if ( 𝑦 = 0 , 0 , 1 ) = 1 )
30 28 29 sylan9eq ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → ( 𝐹 ‘ 𝑦 ) = 1 )
31 30 3adant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → ( 𝐹 ‘ 𝑦 ) = 1 )
32 23 31 breqtrrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑦 ) )
33 1t1e1 ⊢ ( 1 · 1 ) = 1
34 33 eqcomi ⊢ 1 = ( 1 · 1 )
35 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑅 ∈ Ring )
36 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑦 ∈ 𝐵 )
37 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑧 ∈ 𝐵 )
38 2 5 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 · 𝑧 ) ∈ 𝐵 )
39 35 36 37 38 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝐵 )
40 eqeq1 ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 · 𝑧 ) = 0 ) )
41 40 ifbid ⊢ ( 𝑥 = ( 𝑦 · 𝑧 ) → if ( 𝑥 = 0 , 0 , 1 ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) )
42 20 26 ifex ⊢ if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) ∈ V
43 41 4 42 fvmpt ⊢ ( ( 𝑦 · 𝑧 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) )
44 39 43 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) )
45 7 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ¬ ( 𝑦 · 𝑧 ) = 0 )
46 45 iffalsed ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( ( 𝑦 · 𝑧 ) = 0 , 0 , 1 ) = 1 )
47 44 46 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = 1 )
48 36 28 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 = 0 , 0 , 1 ) )
49 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑦 ≠ 0 )
50 49 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ¬ 𝑦 = 0 )
51 50 iffalsed ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( 𝑦 = 0 , 0 , 1 ) = 1 )
52 48 51 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑦 ) = 1 )
53 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 0 ↔ 𝑧 = 0 ) )
54 53 ifbid ⊢ ( 𝑥 = 𝑧 → if ( 𝑥 = 0 , 0 , 1 ) = if ( 𝑧 = 0 , 0 , 1 ) )
55 20 26 ifex ⊢ if ( 𝑧 = 0 , 0 , 1 ) ∈ V
56 54 4 55 fvmpt ⊢ ( 𝑧 ∈ 𝐵 → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 = 0 , 0 , 1 ) )
57 37 56 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) = if ( 𝑧 = 0 , 0 , 1 ) )
58 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑧 ≠ 0 )
59 58 neneqd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ¬ 𝑧 = 0 )
60 59 iffalsed ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( 𝑧 = 0 , 0 , 1 ) = 1 )
61 57 60 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ 𝑧 ) = 1 )
62 52 61 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) = ( 1 · 1 ) )
63 34 47 62 3eqtr4a ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 · 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) · ( 𝐹 ‘ 𝑧 ) ) )
64 breq1 ⊢ ( 0 = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) → ( 0 ≤ 2 ↔ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ 2 ) )
65 breq1 ⊢ ( 1 = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) → ( 1 ≤ 2 ↔ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ 2 ) )
66 0le2 ⊢ 0 ≤ 2
67 1le2 ⊢ 1 ≤ 2
68 64 65 66 67 keephyp ⊢ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ 2
69 df-2 ⊢ 2 = ( 1 + 1 )
70 68 69 breqtri ⊢ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ ( 1 + 1 )
71 70 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ≤ ( 1 + 1 ) )
72 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
73 6 72 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
74 73 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → 𝑅 ∈ Grp )
75 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
76 2 75 grpcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
77 74 36 37 76 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 )
78 eqeq1 ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) → ( 𝑥 = 0 ↔ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 ) )
79 78 ifbid ⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) → if ( 𝑥 = 0 , 0 , 1 ) = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) )
80 20 26 ifex ⊢ if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) ∈ V
81 79 4 80 fvmpt ⊢ ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) )
82 77 81 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = if ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) = 0 , 0 , 1 ) )
83 52 61 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) = ( 1 + 1 ) )
84 71 82 83 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) ≤ ( ( 𝐹 ‘ 𝑦 ) + ( 𝐹 ‘ 𝑧 ) ) )
85 8 9 10 11 12 6 17 22 32 63 84 isabvd ⊢ ( 𝜑 → 𝐹 ∈ 𝐴 )