Step | Hyp | Ref
| Expression |
1 | | perpcom.1 |
. 2
⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) |
2 | | incom 4031 |
. . . . 5
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)) |
4 | | ralcom 3307 |
. . . . 5
⊢
(∀𝑢 ∈
𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐴 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) |
5 | | isperp.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
6 | | isperp.d |
. . . . . . . 8
⊢ − =
(dist‘𝐺) |
7 | | isperp.i |
. . . . . . . 8
⊢ 𝐼 = (Itv‘𝐺) |
8 | | isperp.l |
. . . . . . . 8
⊢ 𝐿 = (LineG‘𝐺) |
9 | | eqid 2824 |
. . . . . . . 8
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
10 | | isperp.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
11 | 10 | ad3antrrr 723 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝐺 ∈ TarskiG) |
12 | | isperp.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
13 | 12 | ad3antrrr 723 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝐴 ∈ ran 𝐿) |
14 | | simplrr 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑢 ∈ 𝐴) |
15 | 5, 8, 7, 11, 13, 14 | tglnpt 25860 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑢 ∈ 𝑃) |
16 | | inss1 4056 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
17 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑥 ∈ (𝐴 ∩ 𝐵)) |
18 | 16, 17 | sseldi 3824 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑥 ∈ 𝐴) |
19 | 5, 8, 7, 11, 13, 18 | tglnpt 25860 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑥 ∈ 𝑃) |
20 | | isperp.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ran 𝐿) |
21 | 20 | ad3antrrr 723 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝐵 ∈ ran 𝐿) |
22 | | simplrl 797 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑣 ∈ 𝐵) |
23 | 5, 8, 7, 11, 21, 22 | tglnpt 25860 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 𝑣 ∈ 𝑃) |
24 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) |
25 | 5, 6, 7, 8, 9, 11,
15, 19, 23, 24 | ragcom 26009 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) → 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) |
26 | 10 | ad3antrrr 723 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝐺 ∈ TarskiG) |
27 | 20 | ad3antrrr 723 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝐵 ∈ ran 𝐿) |
28 | | simplrl 797 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑣 ∈ 𝐵) |
29 | 5, 8, 7, 26, 27, 28 | tglnpt 25860 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑣 ∈ 𝑃) |
30 | 12 | ad3antrrr 723 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝐴 ∈ ran 𝐿) |
31 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑥 ∈ (𝐴 ∩ 𝐵)) |
32 | 16, 31 | sseldi 3824 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑥 ∈ 𝐴) |
33 | 5, 8, 7, 26, 30, 32 | tglnpt 25860 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑥 ∈ 𝑃) |
34 | | simplrr 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑢 ∈ 𝐴) |
35 | 5, 8, 7, 26, 30, 34 | tglnpt 25860 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 𝑢 ∈ 𝑃) |
36 | | simpr 479 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) |
37 | 5, 6, 7, 8, 9, 26,
29, 33, 35, 36 | ragcom 26009 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) ∧ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺)) → 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) |
38 | 25, 37 | impbida 837 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ (𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐴)) → (〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺))) |
39 | 38 | 2ralbidva 3196 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → (∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐴 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐴 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺))) |
40 | 4, 39 | syl5bb 275 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐴 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺))) |
41 | 3, 40 | rexeqbidva 3366 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺) ↔ ∃𝑥 ∈ (𝐵 ∩ 𝐴)∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐴 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺))) |
42 | 5, 6, 7, 8, 10, 12, 20 | isperp 26023 |
. . 3
⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
43 | 5, 6, 7, 8, 10, 20, 12 | isperp 26023 |
. . 3
⊢ (𝜑 → (𝐵(⟂G‘𝐺)𝐴 ↔ ∃𝑥 ∈ (𝐵 ∩ 𝐴)∀𝑣 ∈ 𝐵 ∀𝑢 ∈ 𝐴 〈“𝑣𝑥𝑢”〉 ∈ (∟G‘𝐺))) |
44 | 41, 42, 43 | 3bitr4d 303 |
. 2
⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ 𝐵(⟂G‘𝐺)𝐴)) |
45 | 1, 44 | mpbid 224 |
1
⊢ (𝜑 → 𝐵(⟂G‘𝐺)𝐴) |