| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
| 2 | | rlocval.1 |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 3 | 2 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 4 | 3 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝐵 ∈ V) |
| 5 | | erlval.20 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 6 | 5 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑆 ⊆ 𝐵) |
| 7 | 4, 6 | ssexd 5324 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑆 ∈ V) |
| 8 | | erlval.q |
. . . 4
⊢ ∼ =
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} |
| 9 | | erlval.w |
. . . . . . 7
⊢ 𝑊 = (𝐵 × 𝑆) |
| 10 | 4, 7 | xpexd 7771 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (𝐵 × 𝑆) ∈ V) |
| 11 | 9, 10 | eqeltrid 2845 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑊 ∈ V) |
| 12 | 11, 11 | xpexd 7771 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (𝑊 × 𝑊) ∈ V) |
| 13 | | simprll 779 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )) → 𝑎 ∈ 𝑊) |
| 14 | | simprlr 780 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )) → 𝑏 ∈ 𝑊) |
| 15 | 13, 14 | opabssxpd 5732 |
. . . . . 6
⊢ (𝜑 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} ⊆ (𝑊 × 𝑊)) |
| 16 | 15 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} ⊆ (𝑊 × 𝑊)) |
| 17 | 12, 16 | ssexd 5324 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ∈ V) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )} ∈
V) |
| 18 | 8, 17 | eqeltrid 2845 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ∼ ∈
V) |
| 19 | | fvexd 6921 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) ∈ V) |
| 20 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
| 21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = (.r‘𝑅)) |
| 22 | | rlocval.3 |
. . . . . 6
⊢ · =
(.r‘𝑅) |
| 23 | 21, 22 | eqtr4di 2795 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = · ) |
| 24 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
(Base‘𝑟) ∈
V) |
| 25 | | vex 3484 |
. . . . . . . 8
⊢ 𝑠 ∈ V |
| 26 | 25 | a1i 11 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 ∈ V) |
| 27 | 24, 26 | xpexd 7771 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
((Base‘𝑟) ×
𝑠) ∈
V) |
| 28 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
| 29 | 28 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
(Base‘𝑟) =
(Base‘𝑅)) |
| 30 | 29, 2 | eqtr4di 2795 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
(Base‘𝑟) = 𝐵) |
| 31 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 = 𝑆) |
| 32 | 30, 31 | xpeq12d 5716 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
((Base‘𝑟) ×
𝑠) = (𝐵 × 𝑆)) |
| 33 | 32, 9 | eqtr4di 2795 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
((Base‘𝑟) ×
𝑠) = 𝑊) |
| 34 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊) |
| 35 | 34 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤 ↔ 𝑎 ∈ 𝑊)) |
| 36 | 34 | eleq2d 2827 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑊)) |
| 37 | 35, 36 | anbi12d 632 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ↔ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊))) |
| 38 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑠 = 𝑆) |
| 39 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑥 = · ) |
| 40 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑡 = 𝑡) |
| 41 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = 𝑅 → (-g‘𝑟) = (-g‘𝑅)) |
| 42 | 41 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (-g‘𝑟) = (-g‘𝑅)) |
| 43 | | rlocval.4 |
. . . . . . . . . . . . . 14
⊢ − =
(-g‘𝑅) |
| 44 | 42, 43 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (-g‘𝑟) = − ) |
| 45 | 39 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(2nd ‘𝑏)) = ((1st ‘𝑎) · (2nd
‘𝑏))) |
| 46 | 39 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑏)𝑥(2nd ‘𝑎)) = ((1st ‘𝑏) · (2nd
‘𝑎))) |
| 47 | 44, 45, 46 | oveq123d 7452 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd
‘𝑏)) −
((1st ‘𝑏)
·
(2nd ‘𝑎)))) |
| 48 | 39, 40, 47 | oveq123d 7452 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎))))) |
| 49 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
| 50 | 49 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (0g‘𝑟) = (0g‘𝑅)) |
| 51 | | rlocval.2 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑅) |
| 52 | 50, 51 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (0g‘𝑟) = 0 ) |
| 53 | 48, 52 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟) ↔ (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )) |
| 54 | 38, 53 | rexeqbidv 3347 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟) ↔ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )) |
| 55 | 37, 54 | anbi12d 632 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟)) ↔ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 ))) |
| 56 | 55 | opabbidv 5209 |
. . . . . . 7
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ∃𝑡 ∈ 𝑆 (𝑡 · (((1st
‘𝑎) ·
(2nd ‘𝑏))
−
((1st ‘𝑏)
·
(2nd ‘𝑎)))) = 0 )}) |
| 57 | 56, 8 | eqtr4di 2795 |
. . . . . 6
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))} = ∼ ) |
| 58 | 27, 33, 57 | csbied2 3936 |
. . . . 5
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))} = ∼ ) |
| 59 | 19, 23, 58 | csbied2 3936 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) →
⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))} = ∼ ) |
| 60 | | df-erl 33259 |
. . . 4
⊢
~RL = (𝑟
∈ V, 𝑠 ∈ V
↦ ⦋(.r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ∃𝑡 ∈ 𝑠 (𝑡𝑥(((1st ‘𝑎)𝑥(2nd ‘𝑏))(-g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (0g‘𝑟))}) |
| 61 | 59, 60 | ovmpoga 7587 |
. . 3
⊢ ((𝑅 ∈ V ∧ 𝑆 ∈ V ∧ ∼ ∈
V) → (𝑅
~RL 𝑆) =
∼
) |
| 62 | 1, 7, 18, 61 | syl3anc 1373 |
. 2
⊢ ((𝜑 ∧ 𝑅 ∈ V) → (𝑅 ~RL 𝑆) = ∼ ) |
| 63 | 60 | reldmmpo 7567 |
. . . . 5
⊢ Rel dom
~RL |
| 64 | 63 | ovprc1 7470 |
. . . 4
⊢ (¬
𝑅 ∈ V → (𝑅 ~RL 𝑆) = ∅) |
| 65 | 64 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (𝑅 ~RL 𝑆) = ∅) |
| 66 | 8, 15 | eqsstrid 4022 |
. . . . . 6
⊢ (𝜑 → ∼ ⊆ (𝑊 × 𝑊)) |
| 67 | 66 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → ∼ ⊆ (𝑊 × 𝑊)) |
| 68 | | fvprc 6898 |
. . . . . . . . . . 11
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
| 69 | 2, 68 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
| 70 | 69 | xpeq1d 5714 |
. . . . . . . . 9
⊢ (¬
𝑅 ∈ V → (𝐵 × 𝑆) = (∅ × 𝑆)) |
| 71 | | 0xp 5784 |
. . . . . . . . 9
⊢ (∅
× 𝑆) =
∅ |
| 72 | 70, 71 | eqtrdi 2793 |
. . . . . . . 8
⊢ (¬
𝑅 ∈ V → (𝐵 × 𝑆) = ∅) |
| 73 | 9, 72 | eqtrid 2789 |
. . . . . . 7
⊢ (¬
𝑅 ∈ V → 𝑊 = ∅) |
| 74 | | id 22 |
. . . . . . . . 9
⊢ (𝑊 = ∅ → 𝑊 = ∅) |
| 75 | 74, 74 | xpeq12d 5716 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝑊 × 𝑊) = (∅ ×
∅)) |
| 76 | | 0xp 5784 |
. . . . . . . 8
⊢ (∅
× ∅) = ∅ |
| 77 | 75, 76 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝑊 × 𝑊) = ∅) |
| 78 | 73, 77 | syl 17 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → (𝑊 × 𝑊) = ∅) |
| 79 | 78 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (𝑊 × 𝑊) = ∅) |
| 80 | 67, 79 | sseqtrd 4020 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → ∼ ⊆
∅) |
| 81 | | ss0 4402 |
. . . 4
⊢ ( ∼
⊆ ∅ → ∼ =
∅) |
| 82 | 80, 81 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → ∼ =
∅) |
| 83 | 65, 82 | eqtr4d 2780 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑅 ∈ V) → (𝑅 ~RL 𝑆) = ∼ ) |
| 84 | 62, 83 | pm2.61dan 813 |
1
⊢ (𝜑 → (𝑅 ~RL 𝑆) = ∼ ) |