Step | Hyp | Ref
| Expression |
1 | | isperp.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | isperp.d |
. . . 4
⊢ − =
(dist‘𝐺) |
3 | | isperp.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
4 | | isperp.l |
. . . 4
⊢ 𝐿 = (LineG‘𝐺) |
5 | | eqid 2622 |
. . . 4
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
6 | | isperp.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝐺 ∈ TarskiG) |
8 | | ragperp.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ran 𝐿) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝐵 ∈ ran 𝐿) |
10 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑣 ∈ 𝐵) |
11 | 1, 4, 3, 7, 9, 10 | tglnpt 25444 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑣 ∈ 𝑃) |
12 | | isperp.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ran 𝐿) |
13 | 12 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝐴 ∈ ran 𝐿) |
14 | | inss1 3833 |
. . . . . . 7
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
15 | | ragperp.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵)) |
16 | 14, 15 | sseldi 3601 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
17 | 16 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑋 ∈ 𝐴) |
18 | 1, 4, 3, 7, 13, 17 | tglnpt 25444 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑋 ∈ 𝑃) |
19 | | simprl 794 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑢 ∈ 𝐴) |
20 | 1, 4, 3, 7, 13, 19 | tglnpt 25444 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑢 ∈ 𝑃) |
21 | | ragperp.v |
. . . . . . 7
⊢ (𝜑 → 𝑉 ∈ 𝐵) |
22 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑉 ∈ 𝐵) |
23 | 1, 4, 3, 7, 9, 22 | tglnpt 25444 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑉 ∈ 𝑃) |
24 | | ragperp.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ 𝐴) |
25 | 24 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑈 ∈ 𝐴) |
26 | 1, 4, 3, 7, 13, 25 | tglnpt 25444 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑈 ∈ 𝑃) |
27 | | ragperp.r |
. . . . . . . 8
⊢ (𝜑 → 〈“𝑈𝑋𝑉”〉 ∈ (∟G‘𝐺)) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 〈“𝑈𝑋𝑉”〉 ∈ (∟G‘𝐺)) |
29 | | ragperp.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ≠ 𝑋) |
30 | 29 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑈 ≠ 𝑋) |
31 | 24 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑈 ∈ 𝐴) |
32 | 6 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝐺 ∈ TarskiG) |
33 | 18 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑋 ∈ 𝑃) |
34 | 20 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑢 ∈ 𝑃) |
35 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → ¬ 𝑋 = 𝑢) |
36 | 35 | neqned 2801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑋 ≠ 𝑢) |
37 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝐴 ∈ ran 𝐿) |
38 | 16 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑋 ∈ 𝐴) |
39 | 19 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑢 ∈ 𝐴) |
40 | 1, 3, 4, 32, 33, 34, 36, 36, 37, 38, 39 | tglinethru 25531 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝐴 = (𝑋𝐿𝑢)) |
41 | 31, 40 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑢) → 𝑈 ∈ (𝑋𝐿𝑢)) |
42 | 41 | ex 450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → (¬ 𝑋 = 𝑢 → 𝑈 ∈ (𝑋𝐿𝑢))) |
43 | 42 | orrd 393 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → (𝑋 = 𝑢 ∨ 𝑈 ∈ (𝑋𝐿𝑢))) |
44 | 43 | orcomd 403 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → (𝑈 ∈ (𝑋𝐿𝑢) ∨ 𝑋 = 𝑢)) |
45 | 1, 2, 3, 4, 5, 7, 26, 18, 23, 20, 28, 30, 44 | ragcol 25594 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 〈“𝑢𝑋𝑉”〉 ∈ (∟G‘𝐺)) |
46 | 1, 2, 3, 4, 5, 7, 20, 18, 23, 45 | ragcom 25593 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 〈“𝑉𝑋𝑢”〉 ∈ (∟G‘𝐺)) |
47 | | ragperp.2 |
. . . . . 6
⊢ (𝜑 → 𝑉 ≠ 𝑋) |
48 | 47 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 𝑉 ≠ 𝑋) |
49 | 21 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑉 ∈ 𝐵) |
50 | 6 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝐺 ∈ TarskiG) |
51 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑋 ∈ 𝑃) |
52 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑣 ∈ 𝑃) |
53 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → ¬ 𝑋 = 𝑣) |
54 | 53 | neqned 2801 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑋 ≠ 𝑣) |
55 | 8 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝐵 ∈ ran 𝐿) |
56 | | inss2 3834 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
57 | 56, 15 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
58 | 57 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑋 ∈ 𝐵) |
59 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑣 ∈ 𝐵) |
60 | 1, 3, 4, 50, 51, 52, 54, 54, 55, 58, 59 | tglinethru 25531 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝐵 = (𝑋𝐿𝑣)) |
61 | 49, 60 | eleqtrd 2703 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) ∧ ¬ 𝑋 = 𝑣) → 𝑉 ∈ (𝑋𝐿𝑣)) |
62 | 61 | ex 450 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → (¬ 𝑋 = 𝑣 → 𝑉 ∈ (𝑋𝐿𝑣))) |
63 | 62 | orrd 393 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → (𝑋 = 𝑣 ∨ 𝑉 ∈ (𝑋𝐿𝑣))) |
64 | 63 | orcomd 403 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → (𝑉 ∈ (𝑋𝐿𝑣) ∨ 𝑋 = 𝑣)) |
65 | 1, 2, 3, 4, 5, 7, 23, 18, 20, 11, 46, 48, 64 | ragcol 25594 |
. . . 4
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 〈“𝑣𝑋𝑢”〉 ∈ (∟G‘𝐺)) |
66 | 1, 2, 3, 4, 5, 7, 11, 18, 20, 65 | ragcom 25593 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵)) → 〈“𝑢𝑋𝑣”〉 ∈ (∟G‘𝐺)) |
67 | 66 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑋𝑣”〉 ∈ (∟G‘𝐺)) |
68 | 1, 2, 3, 4, 6, 12,
8, 15 | isperp2 25610 |
. 2
⊢ (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐵 〈“𝑢𝑋𝑣”〉 ∈ (∟G‘𝐺))) |
69 | 67, 68 | mpbird 247 |
1
⊢ (𝜑 → 𝐴(⟂G‘𝐺)𝐵) |