Step | Hyp | Ref
| Expression |
1 | | erldi.4 |
. . 3
⊢ (𝜑 → 𝑈 ∼ 𝑉) |
2 | | erlcl1.e |
. . . . 5
⊢ ∼ =
(𝑅 ~RL
𝑆) |
3 | | erlcl1.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | | erldi.1 |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
5 | | erldi.2 |
. . . . . 6
⊢ · =
(.r‘𝑅) |
6 | | erldi.3 |
. . . . . 6
⊢ − =
(-g‘𝑅) |
7 | | eqid 2740 |
. . . . . 6
⊢ (𝐵 × 𝑆) = (𝐵 × 𝑆) |
8 | | eqid 2740 |
. . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} |
9 | | erlcl1.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
10 | 3, 4, 5, 6, 7, 8, 9 | erlval 33230 |
. . . . 5
⊢ (𝜑 → (𝑅 ~RL 𝑆) = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )}) |
11 | 2, 10 | eqtrid 2792 |
. . . 4
⊢ (𝜑 → ∼ = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝐵 × 𝑆) ∧ 𝑏 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )}) |
12 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → 𝑎 = 𝑈) |
13 | 12 | fveq2d 6924 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (1st ‘𝑎) = (1st ‘𝑈)) |
14 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → 𝑏 = 𝑉) |
15 | 14 | fveq2d 6924 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (2nd ‘𝑏) = (2nd ‘𝑉)) |
16 | 13, 15 | oveq12d 7466 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → ((1st ‘𝑎) · (2nd
‘𝑏)) =
((1st ‘𝑈)
·
(2nd ‘𝑉))) |
17 | 14 | fveq2d 6924 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (1st ‘𝑏) = (1st ‘𝑉)) |
18 | 12 | fveq2d 6924 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (2nd ‘𝑎) = (2nd ‘𝑈)) |
19 | 17, 18 | oveq12d 7466 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → ((1st ‘𝑏) · (2nd
‘𝑎)) =
((1st ‘𝑉)
·
(2nd ‘𝑈))) |
20 | 16, 19 | oveq12d 7466 |
. . . . . . . 8
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (((1st ‘𝑎) · (2nd
‘𝑏)) −
((1st ‘𝑏)
·
(2nd ‘𝑎)))
= (((1st ‘𝑈) · (2nd
‘𝑉)) −
((1st ‘𝑉)
·
(2nd ‘𝑈)))) |
21 | 20 | oveq2d 7464 |
. . . . . . 7
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈))))) |
22 | 21 | eqeq1d 2742 |
. . . . . 6
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → ((𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈)))) = 0 )) |
23 | 22 | rexbidv 3185 |
. . . . 5
⊢ ((𝑎 = 𝑈 ∧ 𝑏 = 𝑉) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈)))) = 0 )) |
24 | 23 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 = 𝑈 ∧ 𝑏 = 𝑉)) → (∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈)))) = 0 )) |
25 | 11, 24 | brab2d 32629 |
. . 3
⊢ (𝜑 → (𝑈 ∼ 𝑉 ↔ ((𝑈 ∈ (𝐵 × 𝑆) ∧ 𝑉 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈)))) = 0 ))) |
26 | 1, 25 | mpbid 232 |
. 2
⊢ (𝜑 → ((𝑈 ∈ (𝐵 × 𝑆) ∧ 𝑉 ∈ (𝐵 × 𝑆)) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈)))) = 0 )) |
27 | 26 | simprd 495 |
1
⊢ (𝜑 → ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑈) ·
(2nd ‘𝑉))
−
((1st ‘𝑉)
·
(2nd ‘𝑈)))) = 0 ) |