Proof of Theorem opphllem6
Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . 4
⊢ 𝑃 = (Base‘𝐺) |
2 | | hpg.d |
. . . 4
⊢ − =
(dist‘𝐺) |
3 | | hpg.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
4 | | opphl.l |
. . . 4
⊢ 𝐿 = (LineG‘𝐺) |
5 | | eqid 2622 |
. . . 4
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
6 | | opphl.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐺 ∈ TarskiG) |
8 | | opphllem5.n |
. . . 4
⊢ 𝑁 = ((pInvG‘𝐺)‘𝑀) |
9 | | opphl.k |
. . . 4
⊢ 𝐾 = (hlG‘𝐺) |
10 | | opphllem5.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ 𝑃) |
11 | 10 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑀 ∈ 𝑃) |
12 | | opphllem5.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
13 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐴 ∈ 𝑃) |
14 | | opphllem5.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
15 | 14 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐶 ∈ 𝑃) |
16 | | opphllem5.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑃) |
17 | 16 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑈 ∈ 𝑃) |
18 | | opphl.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
19 | | opphllem5.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ 𝐷) |
20 | 1, 4, 3, 6, 18, 19 | tglnpt 25444 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝑃) |
21 | | opphllem5.p |
. . . . . . . 8
⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
22 | 4, 6, 21 | perpln2 25606 |
. . . . . . 7
⊢ (𝜑 → (𝐴𝐿𝑅) ∈ ran 𝐿) |
23 | 1, 3, 4, 6, 12, 20, 22 | tglnne 25523 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 𝑅) |
24 | 23 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐴 ≠ 𝑅) |
25 | | opphllem6.v |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘𝑅) = 𝑆) |
26 | 25 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝑁‘𝑅) = 𝑆) |
27 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑅 = 𝑆) |
28 | 26, 27 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝑁‘𝑅) = 𝑅) |
29 | 1, 2, 3, 4, 5, 6, 10, 8, 20 | mirinv 25561 |
. . . . . . 7
⊢ (𝜑 → ((𝑁‘𝑅) = 𝑅 ↔ 𝑀 = 𝑅)) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → ((𝑁‘𝑅) = 𝑅 ↔ 𝑀 = 𝑅)) |
31 | 28, 30 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑀 = 𝑅) |
32 | 24, 31 | neeqtrrd 2868 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐴 ≠ 𝑀) |
33 | | opphllem5.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ 𝐷) |
34 | 1, 4, 3, 6, 18, 33 | tglnpt 25444 |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑃) |
35 | | opphllem5.q |
. . . . . . . 8
⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) |
36 | 4, 6, 35 | perpln2 25606 |
. . . . . . 7
⊢ (𝜑 → (𝐶𝐿𝑆) ∈ ran 𝐿) |
37 | 1, 3, 4, 6, 14, 34, 36 | tglnne 25523 |
. . . . . 6
⊢ (𝜑 → 𝐶 ≠ 𝑆) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐶 ≠ 𝑆) |
39 | 31, 27 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑀 = 𝑆) |
40 | 38, 39 | neeqtrrd 2868 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝐶 ≠ 𝑀) |
41 | | simpr 477 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 = 𝑡) → 𝑅 = 𝑡) |
42 | 6 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG) |
43 | 42 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐺 ∈ TarskiG) |
44 | 14 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐶 ∈ 𝑃) |
45 | 44 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐶 ∈ 𝑃) |
46 | 20 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ 𝑃) |
47 | 46 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ 𝑃) |
48 | 18 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐷 ∈ ran 𝐿) |
49 | | simplr 792 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ 𝐷) |
50 | 1, 4, 3, 42, 48, 49 | tglnpt 25444 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ 𝑃) |
51 | 50 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ 𝑃) |
52 | 12 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐴 ∈ 𝑃) |
53 | 52 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐴 ∈ 𝑃) |
54 | 34 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑆 ∈ 𝑃) |
55 | 54 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑆 ∈ 𝑃) |
56 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 = 𝑆) |
57 | 1, 3, 4, 6, 14, 34, 37 | tglinerflx2 25529 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ (𝐶𝐿𝑆)) |
58 | 57 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑆 ∈ (𝐶𝐿𝑆)) |
59 | 56, 58 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐶𝐿𝑆)) |
60 | 59 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ (𝐶𝐿𝑆)) |
61 | 1, 3, 4, 6, 14, 34, 37 | tgelrnln 25525 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶𝐿𝑆) ∈ ran 𝐿) |
62 | 1, 2, 3, 4, 6, 18,
61, 35 | perpcom 25608 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶𝐿𝑆)(⟂G‘𝐺)𝐷) |
63 | 62 | ad4antr 768 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐶𝐿𝑆)(⟂G‘𝐺)𝐷) |
64 | | simpr 477 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ≠ 𝑡) |
65 | 48 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐷 ∈ ran 𝐿) |
66 | 19 | ad3antrrr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ 𝐷) |
67 | 66 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ 𝐷) |
68 | 49 | adantr 481 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ 𝐷) |
69 | 1, 3, 4, 43, 47, 51, 64, 64, 65, 67, 68 | tglinethru 25531 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐷 = (𝑅𝐿𝑡)) |
70 | 63, 69 | breqtrd 4679 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐶𝐿𝑆)(⟂G‘𝐺)(𝑅𝐿𝑡)) |
71 | 1, 2, 3, 4, 43, 45, 55, 60, 51, 70 | perprag 25618 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 〈“𝐶𝑅𝑡”〉 ∈ (∟G‘𝐺)) |
72 | 1, 3, 4, 6, 12, 20, 23 | tglinerflx2 25529 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ (𝐴𝐿𝑅)) |
73 | 72 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐴𝐿𝑅)) |
74 | 73 | adantr 481 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ (𝐴𝐿𝑅)) |
75 | 1, 3, 4, 6, 12, 20, 23 | tgelrnln 25525 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴𝐿𝑅) ∈ ran 𝐿) |
76 | 1, 2, 3, 4, 6, 18,
75, 21 | perpcom 25608 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴𝐿𝑅)(⟂G‘𝐺)𝐷) |
77 | 76 | ad4antr 768 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐴𝐿𝑅)(⟂G‘𝐺)𝐷) |
78 | 77, 69 | breqtrd 4679 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐴𝐿𝑅)(⟂G‘𝐺)(𝑅𝐿𝑡)) |
79 | 1, 2, 3, 4, 43, 53, 47, 74, 51, 78 | perprag 25618 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 〈“𝐴𝑅𝑡”〉 ∈ (∟G‘𝐺)) |
80 | | simplr 792 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ (𝐴𝐼𝐶)) |
81 | 1, 2, 3, 43, 53, 51, 45, 80 | tgbtwncom 25383 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ (𝐶𝐼𝐴)) |
82 | 1, 2, 3, 4, 5, 43,
45, 47, 51, 53, 71, 79, 81 | ragflat2 25598 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 = 𝑡) |
83 | 41, 82 | pm2.61dane 2881 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 = 𝑡) |
84 | | simpr 477 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ (𝐴𝐼𝐶)) |
85 | 83, 84 | eqeltrd 2701 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐴𝐼𝐶)) |
86 | | opphllem5.o |
. . . . . . . . 9
⊢ (𝜑 → 𝐴𝑂𝐶) |
87 | | hpg.o |
. . . . . . . . . 10
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
88 | 1, 2, 3, 87, 12, 14 | islnopp 25631 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴𝑂𝐶 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶)))) |
89 | 86, 88 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶))) |
90 | 89 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶)) |
91 | 90 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶)) |
92 | 85, 91 | r19.29a 3078 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑅 ∈ (𝐴𝐼𝐶)) |
93 | 31, 92 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑀 ∈ (𝐴𝐼𝐶)) |
94 | 1, 2, 3, 4, 5, 7, 8, 9, 11, 13, 15, 17, 32, 40, 93 | mirbtwnhl 25575 |
. . 3
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝑈(𝐾‘𝑀)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑀)𝐶)) |
95 | 31 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝐾‘𝑀) = (𝐾‘𝑅)) |
96 | 95 | breqd 4664 |
. . 3
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝑈(𝐾‘𝑀)𝐴 ↔ 𝑈(𝐾‘𝑅)𝐴)) |
97 | 39 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝐾‘𝑀) = (𝐾‘𝑆)) |
98 | 97 | breqd 4664 |
. . 3
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → ((𝑁‘𝑈)(𝐾‘𝑀)𝐶 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) |
99 | 94, 96, 98 | 3bitr3d 298 |
. 2
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) |
100 | 18 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐷 ∈ ran 𝐿) |
101 | 6 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐺 ∈ TarskiG) |
102 | 12 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐴 ∈ 𝑃) |
103 | 14 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐶 ∈ 𝑃) |
104 | 19 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑅 ∈ 𝐷) |
105 | 33 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑆 ∈ 𝐷) |
106 | 10 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑀 ∈ 𝑃) |
107 | 86 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐴𝑂𝐶) |
108 | 21 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
109 | 35 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) |
110 | | simpr 477 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑅 ≠ 𝑆) |
111 | 110 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑅 ≠ 𝑆) |
112 | | simpr 477 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) |
113 | 16 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑈 ∈ 𝑃) |
114 | 25 | ad2antrr 762 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → (𝑁‘𝑅) = 𝑆) |
115 | 1, 2, 3, 87, 4, 100, 101, 9, 8, 102, 103, 104, 105, 106, 107, 108, 109, 111, 112, 113, 114 | opphllem3 25641 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) |
116 | 18 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐷 ∈ ran 𝐿) |
117 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝐺 ∈ TarskiG) |
118 | 117 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐺 ∈ TarskiG) |
119 | 14 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐶 ∈ 𝑃) |
120 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝐴 ∈ 𝑃) |
121 | 120 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐴 ∈ 𝑃) |
122 | 33 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑆 ∈ 𝐷) |
123 | 122 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑆 ∈ 𝐷) |
124 | 19 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑅 ∈ 𝐷) |
125 | 124 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑅 ∈ 𝐷) |
126 | 10 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑀 ∈ 𝑃) |
127 | 86 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐴𝑂𝐶) |
128 | 1, 2, 3, 87, 4, 116, 118, 121, 119, 127 | oppcom 25636 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐶𝑂𝐴) |
129 | 35 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) |
130 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
131 | 130 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
132 | 110 | necomd 2849 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑆 ≠ 𝑅) |
133 | 132 | adantr 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑆 ≠ 𝑅) |
134 | | simpr 477 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) |
135 | 16 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑈 ∈ 𝑃) |
136 | 1, 2, 3, 4, 5, 118, 126, 8, 135 | mircl 25556 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑁‘𝑈) ∈ 𝑃) |
137 | 20 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑅 ∈ 𝑃) |
138 | 137 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑅 ∈ 𝑃) |
139 | 25 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑁‘𝑅) = 𝑆) |
140 | 1, 2, 3, 4, 5, 118, 126, 8, 138, 139 | mircom 25558 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑁‘𝑆) = 𝑅) |
141 | 1, 2, 3, 87, 4, 116, 118, 9, 8, 119, 121, 123, 125, 126, 128, 129, 131, 133, 134, 136, 140 | opphllem3 25641 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → ((𝑁‘𝑈)(𝐾‘𝑆)𝐶 ↔ (𝑁‘(𝑁‘𝑈))(𝐾‘𝑅)𝐴)) |
142 | 1, 2, 3, 4, 5, 118, 126, 8, 135 | mirmir 25557 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑁‘(𝑁‘𝑈)) = 𝑈) |
143 | 142 | breq1d 4663 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → ((𝑁‘(𝑁‘𝑈))(𝐾‘𝑅)𝐴 ↔ 𝑈(𝐾‘𝑅)𝐴)) |
144 | 141, 143 | bitr2d 269 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) |
145 | | eqid 2622 |
. . . . 5
⊢
(≤G‘𝐺) =
(≤G‘𝐺) |
146 | 1, 2, 3, 145, 6, 34, 14, 20, 12 | legtrid 25486 |
. . . 4
⊢ (𝜑 → ((𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴) ∨ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶))) |
147 | 146 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → ((𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴) ∨ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶))) |
148 | 115, 144,
147 | mpjaodan 827 |
. 2
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) |
149 | 99, 148 | pm2.61dane 2881 |
1
⊢ (𝜑 → (𝑈(𝐾‘𝑅)𝐴 ↔ (𝑁‘𝑈)(𝐾‘𝑆)𝐶)) |