Proof of Theorem abvtrivd
Step | Hyp | Ref
| Expression |
1 | | abvtriv.a |
. . 3
⊢ 𝐴 = (AbsVal‘𝑅) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝐴 = (AbsVal‘𝑅)) |
3 | | abvtriv.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
5 | | eqidd 2740 |
. 2
⊢ (𝜑 → (+g‘𝑅) = (+g‘𝑅)) |
6 | | abvtrivd.1 |
. . 3
⊢ · =
(.r‘𝑅) |
7 | 6 | a1i 11 |
. 2
⊢ (𝜑 → · =
(.r‘𝑅)) |
8 | | abvtriv.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
9 | 8 | a1i 11 |
. 2
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
10 | | abvtrivd.2 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
11 | | 0re 10734 |
. . . . 5
⊢ 0 ∈
ℝ |
12 | | 1re 10732 |
. . . . 5
⊢ 1 ∈
ℝ |
13 | 11, 12 | ifcli 4471 |
. . . 4
⊢ if(𝑥 = 0 , 0, 1) ∈
ℝ |
14 | 13 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 = 0 , 0, 1) ∈
ℝ) |
15 | | abvtriv.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, 1)) |
16 | 14, 15 | fmptd 6901 |
. 2
⊢ (𝜑 → 𝐹:𝐵⟶ℝ) |
17 | 3, 8 | ring0cl 19454 |
. . 3
⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) |
18 | | iftrue 4430 |
. . . 4
⊢ (𝑥 = 0 → if(𝑥 = 0 , 0, 1) =
0) |
19 | | c0ex 10726 |
. . . 4
⊢ 0 ∈
V |
20 | 18, 15, 19 | fvmpt 6788 |
. . 3
⊢ ( 0 ∈ 𝐵 → (𝐹‘ 0 ) = 0) |
21 | 10, 17, 20 | 3syl 18 |
. 2
⊢ (𝜑 → (𝐹‘ 0 ) = 0) |
22 | | 0lt1 11253 |
. . 3
⊢ 0 <
1 |
23 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = 0 ↔ 𝑦 = 0 )) |
24 | 23 | ifbid 4447 |
. . . . . 6
⊢ (𝑥 = 𝑦 → if(𝑥 = 0 , 0, 1) = if(𝑦 = 0 , 0, 1)) |
25 | | 1ex 10728 |
. . . . . . 7
⊢ 1 ∈
V |
26 | 19, 25 | ifex 4474 |
. . . . . 6
⊢ if(𝑦 = 0 , 0, 1) ∈
V |
27 | 24, 15, 26 | fvmpt 6788 |
. . . . 5
⊢ (𝑦 ∈ 𝐵 → (𝐹‘𝑦) = if(𝑦 = 0 , 0, 1)) |
28 | | ifnefalse 4436 |
. . . . 5
⊢ (𝑦 ≠ 0 → if(𝑦 = 0 , 0, 1) =
1) |
29 | 27, 28 | sylan9eq 2794 |
. . . 4
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → (𝐹‘𝑦) = 1) |
30 | 29 | 3adant1 1131 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → (𝐹‘𝑦) = 1) |
31 | 22, 30 | breqtrrid 5078 |
. 2
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → 0 < (𝐹‘𝑦)) |
32 | | 1t1e1 11891 |
. . . 4
⊢ (1
· 1) = 1 |
33 | 32 | eqcomi 2748 |
. . 3
⊢ 1 = (1
· 1) |
34 | 10 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → 𝑅 ∈ Ring) |
35 | | simp2l 1200 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → 𝑦 ∈ 𝐵) |
36 | | simp3l 1202 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → 𝑧 ∈ 𝐵) |
37 | 3, 6 | ringcl 19446 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦 · 𝑧) ∈ 𝐵) |
38 | 34, 35, 36, 37 | syl3anc 1372 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝑦 · 𝑧) ∈ 𝐵) |
39 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑥 = (𝑦 · 𝑧) → (𝑥 = 0 ↔ (𝑦 · 𝑧) = 0 )) |
40 | 39 | ifbid 4447 |
. . . . . 6
⊢ (𝑥 = (𝑦 · 𝑧) → if(𝑥 = 0 , 0, 1) = if((𝑦 · 𝑧) = 0 , 0, 1)) |
41 | 19, 25 | ifex 4474 |
. . . . . 6
⊢ if((𝑦 · 𝑧) = 0 , 0, 1) ∈
V |
42 | 40, 15, 41 | fvmpt 6788 |
. . . . 5
⊢ ((𝑦 · 𝑧) ∈ 𝐵 → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0 , 0, 1)) |
43 | 38, 42 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘(𝑦 · 𝑧)) = if((𝑦 · 𝑧) = 0 , 0, 1)) |
44 | | abvtrivd.3 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝑦 · 𝑧) ≠ 0 ) |
45 | 44 | neneqd 2940 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → ¬ (𝑦 · 𝑧) = 0 ) |
46 | 45 | iffalsed 4435 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → if((𝑦 · 𝑧) = 0 , 0, 1) =
1) |
47 | 43, 46 | eqtrd 2774 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘(𝑦 · 𝑧)) = 1) |
48 | 35, 27 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘𝑦) = if(𝑦 = 0 , 0, 1)) |
49 | | simp2r 1201 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → 𝑦 ≠ 0 ) |
50 | 49 | neneqd 2940 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → ¬ 𝑦 = 0 ) |
51 | 50 | iffalsed 4435 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → if(𝑦 = 0 , 0, 1) =
1) |
52 | 48, 51 | eqtrd 2774 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘𝑦) = 1) |
53 | | eqeq1 2743 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑥 = 0 ↔ 𝑧 = 0 )) |
54 | 53 | ifbid 4447 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → if(𝑥 = 0 , 0, 1) = if(𝑧 = 0 , 0, 1)) |
55 | 19, 25 | ifex 4474 |
. . . . . . 7
⊢ if(𝑧 = 0 , 0, 1) ∈
V |
56 | 54, 15, 55 | fvmpt 6788 |
. . . . . 6
⊢ (𝑧 ∈ 𝐵 → (𝐹‘𝑧) = if(𝑧 = 0 , 0, 1)) |
57 | 36, 56 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘𝑧) = if(𝑧 = 0 , 0, 1)) |
58 | | simp3r 1203 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → 𝑧 ≠ 0 ) |
59 | 58 | neneqd 2940 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → ¬ 𝑧 = 0 ) |
60 | 59 | iffalsed 4435 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → if(𝑧 = 0 , 0, 1) =
1) |
61 | 57, 60 | eqtrd 2774 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘𝑧) = 1) |
62 | 52, 61 | oveq12d 7201 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → ((𝐹‘𝑦) · (𝐹‘𝑧)) = (1 · 1)) |
63 | 33, 47, 62 | 3eqtr4a 2800 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘(𝑦 · 𝑧)) = ((𝐹‘𝑦) · (𝐹‘𝑧))) |
64 | | breq1 5043 |
. . . . . 6
⊢ (0 =
if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) → (0 ≤ 2
↔ if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) ≤
2)) |
65 | | breq1 5043 |
. . . . . 6
⊢ (1 =
if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) → (1 ≤ 2
↔ if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) ≤
2)) |
66 | | 0le2 11831 |
. . . . . 6
⊢ 0 ≤
2 |
67 | | 1le2 11938 |
. . . . . 6
⊢ 1 ≤
2 |
68 | 64, 65, 66, 67 | keephyp 4495 |
. . . . 5
⊢ if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) ≤
2 |
69 | | df-2 11792 |
. . . . 5
⊢ 2 = (1 +
1) |
70 | 68, 69 | breqtri 5065 |
. . . 4
⊢ if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) ≤ (1 +
1) |
71 | 70 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) ≤ (1 +
1)) |
72 | | ringgrp 19434 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
73 | 10, 72 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Grp) |
74 | 73 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → 𝑅 ∈ Grp) |
75 | | eqid 2739 |
. . . . . 6
⊢
(+g‘𝑅) = (+g‘𝑅) |
76 | 3, 75 | grpcl 18240 |
. . . . 5
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝑅)𝑧) ∈ 𝐵) |
77 | 74, 35, 36, 76 | syl3anc 1372 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝑦(+g‘𝑅)𝑧) ∈ 𝐵) |
78 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑥 = (𝑦(+g‘𝑅)𝑧) → (𝑥 = 0 ↔ (𝑦(+g‘𝑅)𝑧) = 0 )) |
79 | 78 | ifbid 4447 |
. . . . 5
⊢ (𝑥 = (𝑦(+g‘𝑅)𝑧) → if(𝑥 = 0 , 0, 1) = if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1)) |
80 | 19, 25 | ifex 4474 |
. . . . 5
⊢ if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1) ∈
V |
81 | 79, 15, 80 | fvmpt 6788 |
. . . 4
⊢ ((𝑦(+g‘𝑅)𝑧) ∈ 𝐵 → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1)) |
82 | 77, 81 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) = if((𝑦(+g‘𝑅)𝑧) = 0 , 0, 1)) |
83 | 52, 61 | oveq12d 7201 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → ((𝐹‘𝑦) + (𝐹‘𝑧)) = (1 + 1)) |
84 | 71, 82, 83 | 3brtr4d 5072 |
. 2
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ (𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 )) → (𝐹‘(𝑦(+g‘𝑅)𝑧)) ≤ ((𝐹‘𝑦) + (𝐹‘𝑧))) |
85 | 2, 4, 5, 7, 9, 10,
16, 21, 31, 63, 84 | isabvd 19723 |
1
⊢ (𝜑 → 𝐹 ∈ 𝐴) |