Step | Hyp | Ref
| Expression |
1 | | isperp.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
2 | | isperp.i |
. . . . . . 7
⊢ 𝐼 = (Itv‘𝐺) |
3 | | isperp.l |
. . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) |
4 | | isperp.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → 𝐺 ∈ TarskiG) |
6 | 5 | ad5antr 770 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐺 ∈ TarskiG) |
7 | 4 | ad5antr 770 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐺 ∈ TarskiG) |
8 | | isperp.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
9 | 8 | ad5antr 770 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐴 ∈ ran 𝐿) |
10 | | inss1 3833 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
11 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → 𝑥 ∈ (𝐴 ∩ 𝐵)) |
12 | 10, 11 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → 𝑥 ∈ 𝐴) |
13 | 12 | ad4antr 768 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑥 ∈ 𝐴) |
14 | 1, 3, 2, 7, 9, 13 | tglnpt 25444 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑥 ∈ 𝑃) |
15 | 14 | adantl4r 787 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑥 ∈ 𝑃) |
16 | | isperp.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ran 𝐿) |
17 | 16 | ad5antr 770 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐵 ∈ ran 𝐿) |
18 | | simplr 792 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑣 ∈ 𝐵) |
19 | 1, 3, 2, 7, 17, 18 | tglnpt 25444 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑣 ∈ 𝑃) |
20 | 19 | adantl4r 787 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑣 ∈ 𝑃) |
21 | | simp-4r 807 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑢 ∈ 𝐴) |
22 | 1, 3, 2, 7, 9, 21 | tglnpt 25444 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑢 ∈ 𝑃) |
23 | 22 | adantl4r 787 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑢 ∈ 𝑃) |
24 | | isperp.d |
. . . . . . . . 9
⊢ − =
(dist‘𝐺) |
25 | | eqid 2622 |
. . . . . . . . 9
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
26 | | simp-4r 807 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑢 ∈ 𝐴) |
27 | | simplr 792 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑣 ∈ 𝐵) |
28 | | simp-5r 809 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) |
29 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑢 → 𝑦 = 𝑢) |
30 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑢 → 𝑥 = 𝑥) |
31 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑢 → 𝑧 = 𝑧) |
32 | 29, 30, 31 | s3eqd 13609 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑢 → 〈“𝑦𝑥𝑧”〉 = 〈“𝑢𝑥𝑧”〉) |
33 | 32 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑢 → (〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺) ↔ 〈“𝑢𝑥𝑧”〉 ∈ (∟G‘𝐺))) |
34 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑣 → 𝑢 = 𝑢) |
35 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑣 → 𝑥 = 𝑥) |
36 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑣 → 𝑧 = 𝑣) |
37 | 34, 35, 36 | s3eqd 13609 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑣 → 〈“𝑢𝑥𝑧”〉 = 〈“𝑢𝑥𝑣”〉) |
38 | 37 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑣 → (〈“𝑢𝑥𝑧”〉 ∈ (∟G‘𝐺) ↔ 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺))) |
39 | 33, 38 | rspc2va 3323 |
. . . . . . . . . 10
⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) → 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) |
40 | 26, 27, 28, 39 | syl21anc 1325 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 〈“𝑢𝑥𝑣”〉 ∈ (∟G‘𝐺)) |
41 | | simpllr 799 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑥 ≠ 𝑢) |
42 | 41 | necomd 2849 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑢 ≠ 𝑥) |
43 | 42 | adantl4r 787 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑢 ≠ 𝑥) |
44 | | simpr 477 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑥 ≠ 𝑣) |
45 | 44 | necomd 2849 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑣 ≠ 𝑥) |
46 | 45 | adantl4r 787 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑣 ≠ 𝑥) |
47 | 1, 24, 2, 3, 25, 6,
23, 15, 20, 40, 43, 46 | ragncol 25604 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → ¬ (𝑣 ∈ (𝑢𝐿𝑥) ∨ 𝑢 = 𝑥)) |
48 | 1, 3, 2, 6, 23, 15, 20, 47 | ncolrot2 25458 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → ¬ (𝑥 ∈ (𝑣𝐿𝑢) ∨ 𝑣 = 𝑢)) |
49 | 1, 2, 3, 6, 15, 20, 23, 15, 48 | tglineneq 25539 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → (𝑥𝐿𝑣) ≠ (𝑢𝐿𝑥)) |
50 | 49 | necomd 2849 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → (𝑢𝐿𝑥) ≠ (𝑥𝐿𝑣)) |
51 | 1, 2, 3, 7, 22, 14, 42, 42, 9, 21, 13 | tglinethru 25531 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐴 = (𝑢𝐿𝑥)) |
52 | 51 | adantl4r 787 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐴 = (𝑢𝐿𝑥)) |
53 | | inss2 3834 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
54 | 53, 11 | sseldi 3601 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → 𝑥 ∈ 𝐵) |
55 | 54 | ad4antr 768 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝑥 ∈ 𝐵) |
56 | 1, 2, 3, 7, 14, 19, 44, 44, 17, 55, 18 | tglinethru 25531 |
. . . . . 6
⊢
((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐵 = (𝑥𝐿𝑣)) |
57 | 56 | adantl4r 787 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐵 = (𝑥𝐿𝑣)) |
58 | 50, 52, 57 | 3netr4d 2871 |
. . . 4
⊢
(((((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) ∧ 𝑣 ∈ 𝐵) ∧ 𝑥 ≠ 𝑣) → 𝐴 ≠ 𝐵) |
59 | 16 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → 𝐵 ∈ ran 𝐿) |
60 | 1, 2, 3, 5, 59, 54 | tglnpt2 25536 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → ∃𝑣 ∈ 𝐵 𝑥 ≠ 𝑣) |
61 | 60 | ad3antrrr 766 |
. . . 4
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) → ∃𝑣 ∈ 𝐵 𝑥 ≠ 𝑣) |
62 | 58, 61 | r19.29a 3078 |
. . 3
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ≠ 𝑢) → 𝐴 ≠ 𝐵) |
63 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → 𝐴 ∈ ran 𝐿) |
64 | 1, 2, 3, 5, 63, 12 | tglnpt2 25536 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) → ∃𝑢 ∈ 𝐴 𝑥 ≠ 𝑢) |
65 | 64 | adantr 481 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) → ∃𝑢 ∈ 𝐴 𝑥 ≠ 𝑢) |
66 | 62, 65 | r19.29a 3078 |
. 2
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∩ 𝐵)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) → 𝐴 ≠ 𝐵) |
67 | | perpcom.1 |
. . 3
⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) |
68 | 1, 24, 2, 3, 4, 8, 16 | isperp 25607 |
. . 3
⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺))) |
69 | 67, 68 | mpbid 222 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 〈“𝑦𝑥𝑧”〉 ∈ (∟G‘𝐺)) |
70 | 66, 69 | r19.29a 3078 |
1
⊢ (𝜑 → 𝐴 ≠ 𝐵) |