Step | Hyp | Ref
| Expression |
1 | | hpg.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
2 | | hpg.d |
. . . . . . 7
⊢ − =
(dist‘𝐺) |
3 | | hpg.i |
. . . . . . 7
⊢ 𝐼 = (Itv‘𝐺) |
4 | | opphl.l |
. . . . . . 7
⊢ 𝐿 = (LineG‘𝐺) |
5 | | opphl.g |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
6 | | opphl.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
7 | | opphl.k |
. . . . . . 7
⊢ 𝐾 = (hlG‘𝐺) |
8 | | opphllem5.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ 𝐷) |
9 | | opphllem5.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
10 | | opphllem5.u |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ 𝑃) |
11 | | opphllem5.p |
. . . . . . . 8
⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
12 | 1, 4, 3, 5, 6, 8 | tglnpt 26495 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ 𝑃) |
13 | | opphllem5.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈(𝐾‘𝑅)𝐴) |
14 | 1, 3, 7, 10, 9, 12, 5, 13 | hlne2 26552 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ 𝑅) |
15 | 1, 3, 4, 5, 9, 12,
14 | tglinecom 26581 |
. . . . . . . 8
⊢ (𝜑 → (𝐴𝐿𝑅) = (𝑅𝐿𝐴)) |
16 | 11, 15 | breqtrd 5056 |
. . . . . . 7
⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝑅𝐿𝐴)) |
17 | 1, 3, 7, 10, 9, 12, 5, 13 | hlcomd 26550 |
. . . . . . 7
⊢ (𝜑 → 𝐴(𝐾‘𝑅)𝑈) |
18 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
16, 17 | hlperpnel 26671 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑈 ∈ 𝐷) |
19 | 18 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → ¬ 𝑈 ∈ 𝐷) |
20 | | opphllem5.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝐷) |
21 | | opphllem5.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
22 | | opphllem5.v |
. . . . . . 7
⊢ (𝜑 → 𝑉 ∈ 𝑃) |
23 | | opphllem5.q |
. . . . . . . 8
⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) |
24 | 1, 4, 3, 5, 6, 20 | tglnpt 26495 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ 𝑃) |
25 | | opphllem5.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉(𝐾‘𝑆)𝐶) |
26 | 1, 3, 7, 22, 21, 24, 5, 25 | hlne2 26552 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ≠ 𝑆) |
27 | 1, 3, 4, 5, 21, 24, 26 | tglinecom 26581 |
. . . . . . . 8
⊢ (𝜑 → (𝐶𝐿𝑆) = (𝑆𝐿𝐶)) |
28 | 23, 27 | breqtrd 5056 |
. . . . . . 7
⊢ (𝜑 → 𝐷(⟂G‘𝐺)(𝑆𝐿𝐶)) |
29 | 1, 3, 7, 22, 21, 24, 5, 25 | hlcomd 26550 |
. . . . . . 7
⊢ (𝜑 → 𝐶(𝐾‘𝑆)𝑉) |
30 | 1, 2, 3, 4, 5, 6, 7, 20, 21, 22, 28, 29 | hlperpnel 26671 |
. . . . . 6
⊢ (𝜑 → ¬ 𝑉 ∈ 𝐷) |
31 | 30 | ad3antrrr 730 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → ¬ 𝑉 ∈ 𝐷) |
32 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ 𝐷) |
33 | | simpr 488 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 = 𝑡) → 𝑅 = 𝑡) |
34 | | eqid 2738 |
. . . . . . . . 9
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
35 | 5 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐺 ∈ TarskiG) |
36 | 21 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐶 ∈ 𝑃) |
37 | 12 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ 𝑃) |
38 | 5 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG) |
39 | 6 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐷 ∈ ran 𝐿) |
40 | 1, 4, 3, 38, 39, 32 | tglnpt 26495 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ 𝑃) |
41 | 40 | adantr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ 𝑃) |
42 | 9 | ad4antr 732 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐴 ∈ 𝑃) |
43 | 24 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑆 ∈ 𝑃) |
44 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 = 𝑆) |
45 | 1, 3, 4, 5, 21, 24, 26 | tglinerflx2 26580 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ∈ (𝐶𝐿𝑆)) |
46 | 45 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑆 ∈ (𝐶𝐿𝑆)) |
47 | 44, 46 | eqeltrd 2833 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐶𝐿𝑆)) |
48 | 47 | adantr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ (𝐶𝐿𝑆)) |
49 | 4, 5, 23 | perpln2 26657 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶𝐿𝑆) ∈ ran 𝐿) |
50 | 1, 2, 3, 4, 5, 6, 49, 23 | perpcom 26659 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶𝐿𝑆)(⟂G‘𝐺)𝐷) |
51 | 50 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐶𝐿𝑆)(⟂G‘𝐺)𝐷) |
52 | | simpr 488 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ≠ 𝑡) |
53 | 6 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐷 ∈ ran 𝐿) |
54 | 8 | ad4antr 732 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ 𝐷) |
55 | | simpllr 776 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ 𝐷) |
56 | 1, 3, 4, 35, 37, 41, 52, 52, 53, 54, 55 | tglinethru 26582 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝐷 = (𝑅𝐿𝑡)) |
57 | 51, 56 | breqtrd 5056 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐶𝐿𝑆)(⟂G‘𝐺)(𝑅𝐿𝑡)) |
58 | 1, 2, 3, 4, 35, 36, 43, 48, 41, 57 | perprag 26672 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 〈“𝐶𝑅𝑡”〉 ∈ (∟G‘𝐺)) |
59 | 1, 3, 4, 5, 9, 12,
14 | tglinerflx2 26580 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ (𝐴𝐿𝑅)) |
60 | 59 | ad4antr 732 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 ∈ (𝐴𝐿𝑅)) |
61 | 4, 5, 11 | perpln2 26657 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴𝐿𝑅) ∈ ran 𝐿) |
62 | 1, 2, 3, 4, 5, 6, 61, 11 | perpcom 26659 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴𝐿𝑅)(⟂G‘𝐺)𝐷) |
63 | 62 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐴𝐿𝑅)(⟂G‘𝐺)𝐷) |
64 | 63, 56 | breqtrd 5056 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → (𝐴𝐿𝑅)(⟂G‘𝐺)(𝑅𝐿𝑡)) |
65 | 1, 2, 3, 4, 35, 42, 37, 60, 41, 64 | perprag 26672 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 〈“𝐴𝑅𝑡”〉 ∈ (∟G‘𝐺)) |
66 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ (𝐴𝐼𝐶)) |
67 | 1, 2, 3, 35, 42, 41, 36, 66 | tgbtwncom 26434 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑡 ∈ (𝐶𝐼𝐴)) |
68 | 1, 2, 3, 4, 34, 35, 36, 37, 41, 42, 58, 65, 67 | ragflat2 26649 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) ∧ 𝑅 ≠ 𝑡) → 𝑅 = 𝑡) |
69 | 33, 68 | pm2.61dane 3021 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 = 𝑡) |
70 | 9 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐴 ∈ 𝑃) |
71 | 10 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑈 ∈ 𝑃) |
72 | 22 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑉 ∈ 𝑃) |
73 | 12 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ 𝑃) |
74 | 17 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐴(𝐾‘𝑅)𝑈) |
75 | 21 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐶 ∈ 𝑃) |
76 | 25 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑉(𝐾‘𝑆)𝐶) |
77 | 44 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → (𝐾‘𝑅) = (𝐾‘𝑆)) |
78 | 77 | breqd 5041 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → (𝑉(𝐾‘𝑅)𝐶 ↔ 𝑉(𝐾‘𝑆)𝐶)) |
79 | 76, 78 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑉(𝐾‘𝑅)𝐶) |
80 | 1, 3, 7, 72, 75, 73, 38, 79 | hlcomd 26550 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝐶(𝐾‘𝑅)𝑉) |
81 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ (𝐴𝐼𝐶)) |
82 | 69, 81 | eqeltrd 2833 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐴𝐼𝐶)) |
83 | 1, 2, 3, 38, 70, 73, 75, 82 | tgbtwncom 26434 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐶𝐼𝐴)) |
84 | 1, 3, 7, 75, 72, 70, 38, 73, 80, 83 | btwnhl 26560 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝑉𝐼𝐴)) |
85 | 1, 2, 3, 38, 72, 73, 70, 84 | tgbtwncom 26434 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝐴𝐼𝑉)) |
86 | 1, 3, 7, 70, 71, 72, 38, 73, 74, 85 | btwnhl 26560 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑅 ∈ (𝑈𝐼𝑉)) |
87 | 69, 86 | eqeltrrd 2834 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑡 ∈ (𝑈𝐼𝑉)) |
88 | | rspe 3214 |
. . . . . 6
⊢ ((𝑡 ∈ 𝐷 ∧ 𝑡 ∈ (𝑈𝐼𝑉)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑈𝐼𝑉)) |
89 | 32, 87, 88 | syl2anc 587 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑈𝐼𝑉)) |
90 | 19, 31, 89 | jca31 518 |
. . . 4
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → ((¬ 𝑈 ∈ 𝐷 ∧ ¬ 𝑉 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑈𝐼𝑉))) |
91 | | hpg.o |
. . . . . 6
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
92 | 1, 2, 3, 91, 10, 22 | islnopp 26685 |
. . . . 5
⊢ (𝜑 → (𝑈𝑂𝑉 ↔ ((¬ 𝑈 ∈ 𝐷 ∧ ¬ 𝑉 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑈𝐼𝑉)))) |
93 | 92 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → (𝑈𝑂𝑉 ↔ ((¬ 𝑈 ∈ 𝐷 ∧ ¬ 𝑉 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑈𝐼𝑉)))) |
94 | 90, 93 | mpbird 260 |
. . 3
⊢ ((((𝜑 ∧ 𝑅 = 𝑆) ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐶)) → 𝑈𝑂𝑉) |
95 | | opphllem5.o |
. . . . . 6
⊢ (𝜑 → 𝐴𝑂𝐶) |
96 | 1, 2, 3, 91, 9, 21 | islnopp 26685 |
. . . . . 6
⊢ (𝜑 → (𝐴𝑂𝐶 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶)))) |
97 | 95, 96 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶))) |
98 | 97 | simprd 499 |
. . . 4
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶)) |
99 | 98 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐶)) |
100 | 94, 99 | r19.29a 3199 |
. 2
⊢ ((𝜑 ∧ 𝑅 = 𝑆) → 𝑈𝑂𝑉) |
101 | 6 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐷 ∈ ran 𝐿) |
102 | 5 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐺 ∈ TarskiG) |
103 | | eqid 2738 |
. . . . 5
⊢
((pInvG‘𝐺)‘𝑚) = ((pInvG‘𝐺)‘𝑚) |
104 | 9 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐴 ∈ 𝑃) |
105 | 21 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐶 ∈ 𝑃) |
106 | 8 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑅 ∈ 𝐷) |
107 | 20 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑆 ∈ 𝐷) |
108 | | simpllr 776 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑚 ∈ 𝑃) |
109 | 95 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐴𝑂𝐶) |
110 | 11 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
111 | 23 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) |
112 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑅 ≠ 𝑆) |
113 | 112 | ad3antrrr 730 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑅 ≠ 𝑆) |
114 | | simpr 488 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) |
115 | 10 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑈 ∈ 𝑃) |
116 | | simplr 769 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) |
117 | 116 | eqcomd 2744 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → (((pInvG‘𝐺)‘𝑚)‘𝑅) = 𝑆) |
118 | 22 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑉 ∈ 𝑃) |
119 | 13 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑈(𝐾‘𝑅)𝐴) |
120 | 25 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑉(𝐾‘𝑆)𝐶) |
121 | 1, 2, 3, 91, 4, 101, 102, 7, 103, 104, 105, 106, 107, 108, 109, 110, 111, 113, 114, 115, 117, 118, 119, 120 | opphllem4 26696 |
. . . 4
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴)) → 𝑈𝑂𝑉) |
122 | 6 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐷 ∈ ran 𝐿) |
123 | 5 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐺 ∈ TarskiG) |
124 | 22 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑉 ∈ 𝑃) |
125 | 10 | ad4antr 732 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑈 ∈ 𝑃) |
126 | 21 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐶 ∈ 𝑃) |
127 | 9 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐴 ∈ 𝑃) |
128 | 20 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑆 ∈ 𝐷) |
129 | 8 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑅 ∈ 𝐷) |
130 | | simpllr 776 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑚 ∈ 𝑃) |
131 | 95 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐴𝑂𝐶) |
132 | 1, 2, 3, 91, 4, 122, 123, 127, 126, 131 | oppcom 26690 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐶𝑂𝐴) |
133 | 23 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐷(⟂G‘𝐺)(𝐶𝐿𝑆)) |
134 | 11 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝐷(⟂G‘𝐺)(𝐴𝐿𝑅)) |
135 | 112 | necomd 2989 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑆 ≠ 𝑅) |
136 | 135 | ad3antrrr 730 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑆 ≠ 𝑅) |
137 | | simpr 488 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) |
138 | 12 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑅 ∈ 𝑃) |
139 | | simplr 769 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) |
140 | 139 | eqcomd 2744 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (((pInvG‘𝐺)‘𝑚)‘𝑅) = 𝑆) |
141 | 1, 2, 3, 4, 34, 123, 130, 103, 138, 140 | mircom 26609 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → (((pInvG‘𝐺)‘𝑚)‘𝑆) = 𝑅) |
142 | 25 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑉(𝐾‘𝑆)𝐶) |
143 | 13 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑈(𝐾‘𝑅)𝐴) |
144 | 1, 2, 3, 91, 4, 122, 123, 7, 103, 126, 127, 128, 129, 130, 132, 133, 134, 136, 137, 124, 141, 125, 142, 143 | opphllem4 26696 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑉𝑂𝑈) |
145 | 1, 2, 3, 91, 4, 122, 123, 124, 125, 144 | oppcom 26690 |
. . . 4
⊢
(((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) ∧ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶)) → 𝑈𝑂𝑉) |
146 | | eqid 2738 |
. . . . . 6
⊢
(≤G‘𝐺) =
(≤G‘𝐺) |
147 | 1, 2, 3, 146, 5, 24, 21, 12, 9 | legtrid 26537 |
. . . . 5
⊢ (𝜑 → ((𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴) ∨ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶))) |
148 | 147 | ad3antrrr 730 |
. . . 4
⊢ ((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) → ((𝑆 − 𝐶)(≤G‘𝐺)(𝑅 − 𝐴) ∨ (𝑅 − 𝐴)(≤G‘𝐺)(𝑆 − 𝐶))) |
149 | 121, 145,
148 | mpjaodan 958 |
. . 3
⊢ ((((𝜑 ∧ 𝑅 ≠ 𝑆) ∧ 𝑚 ∈ 𝑃) ∧ 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) → 𝑈𝑂𝑉) |
150 | 5 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝐺 ∈ TarskiG) |
151 | 12 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑅 ∈ 𝑃) |
152 | 24 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑆 ∈ 𝑃) |
153 | 1, 2, 3, 91, 4, 6,
5, 9, 21, 95 | opptgdim2 26691 |
. . . . 5
⊢ (𝜑 → 𝐺DimTarskiG≥2) |
154 | 153 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝐺DimTarskiG≥2) |
155 | 1, 2, 3, 4, 150, 34, 151, 152, 154 | midex 26683 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → ∃𝑚 ∈ 𝑃 𝑆 = (((pInvG‘𝐺)‘𝑚)‘𝑅)) |
156 | 149, 155 | r19.29a 3199 |
. 2
⊢ ((𝜑 ∧ 𝑅 ≠ 𝑆) → 𝑈𝑂𝑉) |
157 | 100, 156 | pm2.61dane 3021 |
1
⊢ (𝜑 → 𝑈𝑂𝑉) |