Proof of Theorem colhp
Step | Hyp | Ref
| Expression |
1 | | ancom 454 |
. . 3
⊢ ((𝐴(𝐾‘𝐶)𝐵 ∧ ¬ 𝐴 ∈ 𝐷) ↔ (¬ 𝐴 ∈ 𝐷 ∧ 𝐴(𝐾‘𝐶)𝐵)) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → ((𝐴(𝐾‘𝐶)𝐵 ∧ ¬ 𝐴 ∈ 𝐷) ↔ (¬ 𝐴 ∈ 𝐷 ∧ 𝐴(𝐾‘𝐶)𝐵))) |
3 | | hpgid.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
4 | | hpgid.i |
. . . . 5
⊢ 𝐼 = (Itv‘𝐺) |
5 | | hpgid.l |
. . . . 5
⊢ 𝐿 = (LineG‘𝐺) |
6 | | hpgid.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
7 | 6 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐺 ∈ TarskiG) |
8 | | hpgid.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
9 | 8 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐷 ∈ ran 𝐿) |
10 | | colopp.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
11 | 10 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐵 ∈ 𝑃) |
12 | | hpgid.o |
. . . . 5
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
13 | | eqid 2778 |
. . . . . . 7
⊢
(dist‘𝐺) =
(dist‘𝐺) |
14 | | eqid 2778 |
. . . . . . 7
⊢
(pInvG‘𝐺) =
(pInvG‘𝐺) |
15 | | colopp.p |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
16 | 3, 5, 4, 6, 8, 15 | tglnpt 25900 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
17 | | eqid 2778 |
. . . . . . 7
⊢
((pInvG‘𝐺)‘𝐶) = ((pInvG‘𝐺)‘𝐶) |
18 | | hpgid.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
19 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mircl 26012 |
. . . . . 6
⊢ (𝜑 → (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝑃) |
20 | 19 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝑃) |
21 | 15 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐶 ∈ 𝐷) |
22 | 16 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐶 ∈ 𝑃) |
23 | 18 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐴 ∈ 𝑃) |
24 | | nelne2 3068 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐶 ≠ 𝐴) |
25 | 15, 24 | sylan 575 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐶 ≠ 𝐴) |
26 | 25 | necomd 3024 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐴 ≠ 𝐶) |
27 | 26 | neneqd 2974 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ¬ 𝐴 = 𝐶) |
28 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ¬ 𝐴 ∈ 𝐷) |
29 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mirmir 26013 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((pInvG‘𝐺)‘𝐶)‘(((pInvG‘𝐺)‘𝐶)‘𝐴)) = 𝐴) |
30 | 29 | adantr 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → (((pInvG‘𝐺)‘𝐶)‘(((pInvG‘𝐺)‘𝐶)‘𝐴)) = 𝐴) |
31 | 6 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → 𝐺 ∈ TarskiG) |
32 | 8 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → 𝐷 ∈ ran 𝐿) |
33 | 15 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → 𝐶 ∈ 𝐷) |
34 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) |
35 | 3, 13, 4, 5, 14, 31, 17, 32, 33, 34 | mirln 26027 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → (((pInvG‘𝐺)‘𝐶)‘(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∈ 𝐷) |
36 | 30, 35 | eqeltrrd 2860 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) → 𝐴 ∈ 𝐷) |
37 | 36 | stoic1a 1816 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) |
38 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 = 𝐶) → 𝑡 = 𝐶) |
39 | | eqidd 2779 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 = 𝐶) → (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) = (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
40 | 38, 39 | eleq12d 2853 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 = 𝐶) → (𝑡 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ↔ 𝐶 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)))) |
41 | 3, 13, 4, 5, 14, 6,
16, 17, 18 | mirbtwn 26009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐶 ∈ ((((pInvG‘𝐺)‘𝐶)‘𝐴)𝐼𝐴)) |
42 | 3, 13, 4, 6, 19, 16, 18, 41 | tgbtwncom 25839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
43 | 15, 40, 42 | rspcedvd 3518 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
44 | 43 | adantr 474 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
45 | 28, 37, 44 | jca31 510 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)))) |
46 | 3, 13, 4, 12, 23, 20 | islnopp 26087 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐴𝑂(((pInvG‘𝐺)‘𝐶)‘𝐴) ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))))) |
47 | 45, 46 | mpbird 249 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐴𝑂(((pInvG‘𝐺)‘𝐶)‘𝐴)) |
48 | 3, 13, 4, 12, 5, 9,
7, 23, 20, 47 | oppne3 26091 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐴 ≠ (((pInvG‘𝐺)‘𝐶)‘𝐴)) |
49 | 42 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐶 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
50 | 3, 4, 5, 7, 23, 20, 22, 48, 49 | btwnlng1 25970 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → 𝐶 ∈ (𝐴𝐿(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
51 | 50 | orcd 862 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐶 ∈ (𝐴𝐿(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∨ 𝐴 = (((pInvG‘𝐺)‘𝐶)‘𝐴))) |
52 | 3, 5, 4, 7, 23, 20, 22, 51 | colcom 25909 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐶 ∈ ((((pInvG‘𝐺)‘𝐶)‘𝐴)𝐿𝐴) ∨ (((pInvG‘𝐺)‘𝐶)‘𝐴) = 𝐴)) |
53 | 3, 5, 4, 7, 20, 23, 22, 52 | colrot1 25910 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ((((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶)) |
54 | 53 | orcomd 860 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐴 = 𝐶 ∨ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ (𝐴𝐿𝐶))) |
55 | 54 | ord 853 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (¬ 𝐴 = 𝐶 → (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ (𝐴𝐿𝐶))) |
56 | 27, 55 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ (𝐴𝐿𝐶)) |
57 | | colopp.1 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
58 | 3, 5, 4, 6, 18, 10, 16, 57 | colrot1 25910 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶)) |
59 | 3, 5, 4, 6, 10, 16, 18, 58 | colcom 25909 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵)) |
60 | 59 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵)) |
61 | 3, 4, 5, 7, 20, 23, 22, 11, 56, 60 | coltr 25998 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ((((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵)) |
62 | 3, 5, 4, 7, 22, 11, 20, 61 | colrot1 25910 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐶 ∈ (𝐵𝐿(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∨ 𝐵 = (((pInvG‘𝐺)‘𝐶)‘𝐴))) |
63 | 3, 4, 5, 7, 9, 11,
12, 20, 21, 62 | colopp 26117 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐵𝑂(((pInvG‘𝐺)‘𝐶)‘𝐴) ↔ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷))) |
64 | 3, 4, 5, 12, 7, 9,
23, 11, 20, 47 | lnopp2hpgb 26111 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐵𝑂(((pInvG‘𝐺)‘𝐶)‘𝐴) ↔ 𝐴((hpG‘𝐺)‘𝐷)𝐵)) |
65 | | colhp.k |
. . . . . . . . 9
⊢ 𝐾 = (hlG‘𝐺) |
66 | | simpll 757 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝜑) |
67 | 66, 10 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐵 ∈ 𝑃) |
68 | 66, 18 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐴 ∈ 𝑃) |
69 | 66, 16 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐶 ∈ 𝑃) |
70 | 66, 6 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐺 ∈ TarskiG) |
71 | 66, 15 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐶 ∈ 𝐷) |
72 | | simprr 763 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → ¬ 𝐵 ∈ 𝐷) |
73 | | nelne2 3068 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) → 𝐶 ≠ 𝐵) |
74 | 73 | necomd 3024 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) → 𝐵 ≠ 𝐶) |
75 | 71, 72, 74 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐵 ≠ 𝐶) |
76 | 26 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐴 ≠ 𝐶) |
77 | | simprl 761 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
78 | 3, 13, 4, 5, 14, 70, 17, 65, 69, 67, 68, 68, 75, 76, 77 | mirhl2 26032 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐵(𝐾‘𝐶)𝐴) |
79 | 3, 4, 65, 67, 68, 69, 70, 78 | hlcomd 25955 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → 𝐴(𝐾‘𝐶)𝐵) |
80 | 28 | adantr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → ¬ 𝐴 ∈ 𝐷) |
81 | 79, 80 | jca 507 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷)) → (𝐴(𝐾‘𝐶)𝐵 ∧ ¬ 𝐴 ∈ 𝐷)) |
82 | 81 | 3adantr3 1173 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷)) → (𝐴(𝐾‘𝐶)𝐵 ∧ ¬ 𝐴 ∈ 𝐷)) |
83 | 82 | simpld 490 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷)) → 𝐴(𝐾‘𝐶)𝐵) |
84 | 23 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐴 ∈ 𝑃) |
85 | 11 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐵 ∈ 𝑃) |
86 | 20 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝑃) |
87 | 7 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐺 ∈ TarskiG) |
88 | 16 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐶 ∈ 𝑃) |
89 | | simpr 479 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐴(𝐾‘𝐶)𝐵) |
90 | 42 | ad2antrr 716 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐶 ∈ (𝐴𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
91 | 3, 4, 65, 84, 85, 86, 87, 88, 89, 90 | btwnhl 25965 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴))) |
92 | 3, 4, 65, 84, 85, 88, 87, 5, 89 | hlln 25958 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → 𝐴 ∈ (𝐵𝐿𝐶)) |
93 | 92 | adantr 474 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐴 ∈ (𝐵𝐿𝐶)) |
94 | 87 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐺 ∈ TarskiG) |
95 | 85 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐵 ∈ 𝑃) |
96 | 88 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐶 ∈ 𝑃) |
97 | 84 | adantr 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐴 ∈ 𝑃) |
98 | 89 | adantr 474 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐴(𝐾‘𝐶)𝐵) |
99 | 3, 4, 65, 97, 95, 96, 94, 98 | hlne2 25957 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐵 ≠ 𝐶) |
100 | 9 | ad2antrr 716 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐷 ∈ ran 𝐿) |
101 | | simpr 479 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐵 ∈ 𝐷) |
102 | 15 | ad3antrrr 720 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐶 ∈ 𝐷) |
103 | 3, 4, 5, 94, 95, 96, 99, 99, 100, 101, 102 | tglinethru 25987 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐷 = (𝐵𝐿𝐶)) |
104 | 93, 103 | eleqtrrd 2862 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → 𝐴 ∈ 𝐷) |
105 | 28 | ad2antrr 716 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) ∧ 𝐵 ∈ 𝐷) → ¬ 𝐴 ∈ 𝐷) |
106 | 104, 105 | pm2.65da 807 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → ¬ 𝐵 ∈ 𝐷) |
107 | 37 | adantr 474 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) |
108 | 91, 106, 107 | 3jca 1119 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) ∧ 𝐴(𝐾‘𝐶)𝐵) → (𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷)) |
109 | 83, 108 | impbida 791 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → ((𝐶 ∈ (𝐵𝐼(((pInvG‘𝐺)‘𝐶)‘𝐴)) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ (((pInvG‘𝐺)‘𝐶)‘𝐴) ∈ 𝐷) ↔ 𝐴(𝐾‘𝐶)𝐵)) |
110 | 63, 64, 109 | 3bitr3d 301 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐴 ∈ 𝐷) → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ 𝐴(𝐾‘𝐶)𝐵)) |
111 | 110 | pm5.32da 574 |
. 2
⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ↔ (¬ 𝐴 ∈ 𝐷 ∧ 𝐴(𝐾‘𝐶)𝐵))) |
112 | | simpr 479 |
. . . 4
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐴((hpG‘𝐺)‘𝐷)𝐵) |
113 | 112 | adantrl 706 |
. . 3
⊢ ((𝜑 ∧ (¬ 𝐴 ∈ 𝐷 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵)) → 𝐴((hpG‘𝐺)‘𝐷)𝐵) |
114 | 6 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐺 ∈ TarskiG) |
115 | 8 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐷 ∈ ran 𝐿) |
116 | 18 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐴 ∈ 𝑃) |
117 | 10 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐵 ∈ 𝑃) |
118 | 3, 4, 5, 12, 114, 115, 116, 117, 112 | hpgne1 26109 |
. . . 4
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → ¬ 𝐴 ∈ 𝐷) |
119 | 118, 112 | jca 507 |
. . 3
⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → (¬ 𝐴 ∈ 𝐷 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵)) |
120 | 113, 119 | impbida 791 |
. 2
⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ↔ 𝐴((hpG‘𝐺)‘𝐷)𝐵)) |
121 | 2, 111, 120 | 3bitr2rd 300 |
1
⊢ (𝜑 → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ (𝐴(𝐾‘𝐶)𝐵 ∧ ¬ 𝐴 ∈ 𝐷))) |