Proof of Theorem isabvd
Step | Hyp | Ref
| Expression |
1 | | isabvd.2 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐵⟶ℝ) |
2 | | isabvd.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
3 | 2 | feq2d 6484 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐵⟶ℝ ↔ 𝐹:(Base‘𝑅)⟶ℝ)) |
4 | 1, 3 | mpbid 235 |
. . . . 5
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶ℝ) |
5 | 4 | ffnd 6499 |
. . . 4
⊢ (𝜑 → 𝐹 Fn (Base‘𝑅)) |
6 | 4 | ffvelrnda 6855 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ ℝ) |
7 | | 0le0 11810 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
8 | | isabvd.z |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 =
(0g‘𝑅)) |
9 | 8 | fveq2d 6672 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘ 0 ) = (𝐹‘(0g‘𝑅))) |
10 | | isabvd.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘ 0 ) = 0) |
11 | 9, 10 | eqtr3d 2775 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(0g‘𝑅)) = 0) |
12 | 7, 11 | breqtrrid 5065 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝐹‘(0g‘𝑅))) |
13 | 12 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 0 ≤ (𝐹‘(0g‘𝑅))) |
14 | | fveq2 6668 |
. . . . . . . . 9
⊢ (𝑥 = (0g‘𝑅) → (𝐹‘𝑥) = (𝐹‘(0g‘𝑅))) |
15 | 14 | breq2d 5039 |
. . . . . . . 8
⊢ (𝑥 = (0g‘𝑅) → (0 ≤ (𝐹‘𝑥) ↔ 0 ≤ (𝐹‘(0g‘𝑅)))) |
16 | 13, 15 | syl5ibrcom 250 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 = (0g‘𝑅) → 0 ≤ (𝐹‘𝑥))) |
17 | | simp1 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 𝜑) |
18 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
19 | 2 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 𝐵 = (Base‘𝑅)) |
20 | 18, 19 | eleqtrrd 2836 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 𝑥 ∈ 𝐵) |
21 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 𝑥 ≠ (0g‘𝑅)) |
22 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 0 =
(0g‘𝑅)) |
23 | 21, 22 | neeqtrrd 3008 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 𝑥 ≠ 0 ) |
24 | | isabvd.4 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → 0 < (𝐹‘𝑥)) |
25 | 17, 20, 23, 24 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 0 < (𝐹‘𝑥)) |
26 | | 0re 10714 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
27 | 6 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → (𝐹‘𝑥) ∈ ℝ) |
28 | | ltle 10800 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ (𝐹‘𝑥) ∈ ℝ) → (0 < (𝐹‘𝑥) → 0 ≤ (𝐹‘𝑥))) |
29 | 26, 27, 28 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → (0 < (𝐹‘𝑥) → 0 ≤ (𝐹‘𝑥))) |
30 | 25, 29 | mpd 15 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → 0 ≤ (𝐹‘𝑥)) |
31 | 30 | 3expia 1122 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 ≠ (0g‘𝑅) → 0 ≤ (𝐹‘𝑥))) |
32 | 16, 31 | pm2.61dne 3020 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 0 ≤ (𝐹‘𝑥)) |
33 | | elrege0 12921 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥))) |
34 | 6, 32, 33 | sylanbrc 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ (0[,)+∞)) |
35 | 34 | ralrimiva 3096 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(𝐹‘𝑥) ∈ (0[,)+∞)) |
36 | | ffnfv 6886 |
. . . 4
⊢ (𝐹:(Base‘𝑅)⟶(0[,)+∞) ↔ (𝐹 Fn (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)(𝐹‘𝑥) ∈ (0[,)+∞))) |
37 | 5, 35, 36 | sylanbrc 586 |
. . 3
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(0[,)+∞)) |
38 | 25 | gt0ne0d 11275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑥 ≠ (0g‘𝑅)) → (𝐹‘𝑥) ≠ 0) |
39 | 38 | 3expia 1122 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 ≠ (0g‘𝑅) → (𝐹‘𝑥) ≠ 0)) |
40 | 39 | necon4d 2958 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) = 0 → 𝑥 = (0g‘𝑅))) |
41 | 11 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐹‘(0g‘𝑅)) = 0) |
42 | | fveqeq2 6677 |
. . . . . . 7
⊢ (𝑥 = (0g‘𝑅) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(0g‘𝑅)) = 0)) |
43 | 41, 42 | syl5ibrcom 250 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥 = (0g‘𝑅) → (𝐹‘𝑥) = 0)) |
44 | 40, 43 | impbid 215 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅))) |
45 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘(0g‘𝑅)) = 0) |
46 | 45 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘(0g‘𝑅)) = 0) |
47 | | oveq1 7171 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥(.r‘𝑅)𝑦) = ((0g‘𝑅)(.r‘𝑅)𝑦)) |
48 | | isabvd.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ Ring) |
49 | 48 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
50 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑦 ∈ (Base‘𝑅)) |
51 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑅) =
(Base‘𝑅) |
52 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(.r‘𝑅) = (.r‘𝑅) |
53 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝑅) = (0g‘𝑅) |
54 | 51, 52, 53 | ringlz 19452 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Base‘𝑅)) →
((0g‘𝑅)(.r‘𝑅)𝑦) = (0g‘𝑅)) |
55 | 49, 50, 54 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑦) = (0g‘𝑅)) |
56 | 47, 55 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝑥(.r‘𝑅)𝑦) = (0g‘𝑅)) |
57 | 56 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = (𝐹‘(0g‘𝑅))) |
58 | 14, 45 | sylan9eqr 2795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘𝑥) = 0) |
59 | 58 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → ((𝐹‘𝑥) · (𝐹‘𝑦)) = (0 · (𝐹‘𝑦))) |
60 | 4 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝐹:(Base‘𝑅)⟶ℝ) |
61 | 60, 50 | ffvelrnd 6856 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘𝑦) ∈ ℝ) |
62 | 61 | recnd 10740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘𝑦) ∈ ℂ) |
63 | 62 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘𝑦) ∈ ℂ) |
64 | 63 | mul02d 10909 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (0 · (𝐹‘𝑦)) = 0) |
65 | 59, 64 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → ((𝐹‘𝑥) · (𝐹‘𝑦)) = 0) |
66 | 46, 57, 65 | 3eqtr4d 2783 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
67 | 45 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘(0g‘𝑅)) = 0) |
68 | | oveq2 7172 |
. . . . . . . . . . . 12
⊢ (𝑦 = (0g‘𝑅) → (𝑥(.r‘𝑅)𝑦) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
69 | | simp2 1138 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
70 | 51, 52, 53 | ringrz 19453 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
71 | 49, 69, 70 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
72 | 68, 71 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝑥(.r‘𝑅)𝑦) = (0g‘𝑅)) |
73 | 72 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = (𝐹‘(0g‘𝑅))) |
74 | | fveq2 6668 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (0g‘𝑅) → (𝐹‘𝑦) = (𝐹‘(0g‘𝑅))) |
75 | 74, 45 | sylan9eqr 2795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘𝑦) = 0) |
76 | 75 | oveq2d 7180 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → ((𝐹‘𝑥) · (𝐹‘𝑦)) = ((𝐹‘𝑥) · 0)) |
77 | 60, 69 | ffvelrnd 6856 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ ℝ) |
78 | 77 | recnd 10740 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘𝑥) ∈ ℂ) |
79 | 78 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘𝑥) ∈ ℂ) |
80 | 79 | mul01d 10910 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → ((𝐹‘𝑥) · 0) = 0) |
81 | 76, 80 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → ((𝐹‘𝑥) · (𝐹‘𝑦)) = 0) |
82 | 67, 73, 81 | 3eqtr4d 2783 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
83 | | simpl1 1192 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝜑) |
84 | | isabvd.t |
. . . . . . . . . . . . 13
⊢ (𝜑 → · =
(.r‘𝑅)) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → · =
(.r‘𝑅)) |
86 | 85 | oveqd 7181 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝑥 · 𝑦) = (𝑥(.r‘𝑅)𝑦)) |
87 | 86 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥 · 𝑦)) = (𝐹‘(𝑥(.r‘𝑅)𝑦))) |
88 | | simpl2 1193 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑥 ∈ (Base‘𝑅)) |
89 | 83, 2 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝐵 = (Base‘𝑅)) |
90 | 88, 89 | eleqtrrd 2836 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑥 ∈ 𝐵) |
91 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑥 ≠ (0g‘𝑅)) |
92 | 83, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 0 =
(0g‘𝑅)) |
93 | 91, 92 | neeqtrrd 3008 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑥 ≠ 0 ) |
94 | | simpl3 1194 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑦 ∈ (Base‘𝑅)) |
95 | 94, 89 | eleqtrrd 2836 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑦 ∈ 𝐵) |
96 | | simprr 773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑦 ≠ (0g‘𝑅)) |
97 | 96, 92 | neeqtrrd 3008 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → 𝑦 ≠ 0 ) |
98 | | isabvd.5 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
99 | 83, 90, 93, 95, 97, 98 | syl122anc 1380 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥 · 𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
100 | 87, 99 | eqtr3d 2775 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
101 | 66, 82, 100 | pm2.61da2ne 3022 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦))) |
102 | | oveq1 7171 |
. . . . . . . . . . . 12
⊢ (𝑥 = (0g‘𝑅) → (𝑥(+g‘𝑅)𝑦) = ((0g‘𝑅)(+g‘𝑅)𝑦)) |
103 | | ringgrp 19414 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
104 | 49, 103 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → 𝑅 ∈ Grp) |
105 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(+g‘𝑅) = (+g‘𝑅) |
106 | 51, 105, 53 | grplid 18244 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧ 𝑦 ∈ (Base‘𝑅)) →
((0g‘𝑅)(+g‘𝑅)𝑦) = 𝑦) |
107 | 104, 50, 106 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ((0g‘𝑅)(+g‘𝑅)𝑦) = 𝑦) |
108 | 102, 107 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝑥(+g‘𝑅)𝑦) = 𝑦) |
109 | 108 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) = (𝐹‘𝑦)) |
110 | 7, 58 | breqtrrid 5065 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → 0 ≤ (𝐹‘𝑥)) |
111 | 61, 77 | addge02d 11300 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (0 ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) |
112 | 111 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (0 ≤ (𝐹‘𝑥) ↔ (𝐹‘𝑦) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) |
113 | 110, 112 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘𝑦) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
114 | 109, 113 | eqbrtrd 5049 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑥 = (0g‘𝑅)) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
115 | | oveq2 7172 |
. . . . . . . . . . . 12
⊢ (𝑦 = (0g‘𝑅) → (𝑥(+g‘𝑅)𝑦) = (𝑥(+g‘𝑅)(0g‘𝑅))) |
116 | 51, 105, 53 | grprid 18245 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(+g‘𝑅)(0g‘𝑅)) = 𝑥) |
117 | 104, 69, 116 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝑥(+g‘𝑅)(0g‘𝑅)) = 𝑥) |
118 | 115, 117 | sylan9eqr 2795 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝑥(+g‘𝑅)𝑦) = 𝑥) |
119 | 118 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) = (𝐹‘𝑥)) |
120 | 7, 75 | breqtrrid 5065 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → 0 ≤ (𝐹‘𝑦)) |
121 | 77, 61 | addge01d 11299 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (0 ≤ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) |
122 | 121 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (0 ≤ (𝐹‘𝑦) ↔ (𝐹‘𝑥) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) |
123 | 120, 122 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘𝑥) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
124 | 119, 123 | eqbrtrd 5049 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ 𝑦 = (0g‘𝑅)) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
125 | | isabvd.p |
. . . . . . . . . . . . 13
⊢ (𝜑 → + =
(+g‘𝑅)) |
126 | 83, 125 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → + =
(+g‘𝑅)) |
127 | 126 | oveqd 7181 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
128 | 127 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+g‘𝑅)𝑦))) |
129 | | isabvd.6 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
130 | 83, 90, 93, 95, 97, 129 | syl122anc 1380 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥 + 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
131 | 128, 130 | eqbrtrrd 5051 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) ∧ (𝑥 ≠ (0g‘𝑅) ∧ 𝑦 ≠ (0g‘𝑅))) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
132 | 114, 124,
131 | pm2.61da2ne 3022 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) |
133 | 101, 132 | jca 515 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)) → ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) |
134 | 133 | 3expia 1122 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑦 ∈ (Base‘𝑅) → ((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))) |
135 | 134 | ralrimiv 3095 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ∀𝑦 ∈ (Base‘𝑅)((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦)))) |
136 | 44, 135 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))) |
137 | 136 | ralrimiva 3096 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)(((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))) |
138 | | eqid 2738 |
. . . . 5
⊢
(AbsVal‘𝑅) =
(AbsVal‘𝑅) |
139 | 138, 51, 105, 52, 53 | isabv 19702 |
. . . 4
⊢ (𝑅 ∈ Ring → (𝐹 ∈ (AbsVal‘𝑅) ↔ (𝐹:(Base‘𝑅)⟶(0[,)+∞) ∧ ∀𝑥 ∈ (Base‘𝑅)(((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) |
140 | 48, 139 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (AbsVal‘𝑅) ↔ (𝐹:(Base‘𝑅)⟶(0[,)+∞) ∧ ∀𝑥 ∈ (Base‘𝑅)(((𝐹‘𝑥) = 0 ↔ 𝑥 = (0g‘𝑅)) ∧ ∀𝑦 ∈ (Base‘𝑅)((𝐹‘(𝑥(.r‘𝑅)𝑦)) = ((𝐹‘𝑥) · (𝐹‘𝑦)) ∧ (𝐹‘(𝑥(+g‘𝑅)𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))))))) |
141 | 37, 137, 140 | mpbir2and 713 |
. 2
⊢ (𝜑 → 𝐹 ∈ (AbsVal‘𝑅)) |
142 | | isabvd.a |
. 2
⊢ (𝜑 → 𝐴 = (AbsVal‘𝑅)) |
143 | 141, 142 | eleqtrrd 2836 |
1
⊢ (𝜑 → 𝐹 ∈ 𝐴) |