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 ( 𝜑𝐹𝐴 )