Metamath Proof Explorer

Theorem colhp

Description: Half-plane relation for colinear points. Theorem 9.19 of Schwabhauser p. 73. (Contributed by Thierry Arnoux, 3-Aug-2020)

Ref Expression
Hypotheses hpgid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
hpgid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hpgid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
hpgid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hpgid.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
hpgid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hpgid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
colopp.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
colopp.p ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
colopp.1 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
colhp.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
Assertion colhp ( 𝜑 → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ↔ ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ∧ ¬ 𝐴 ∈ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 hpgid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hpgid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 hpgid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 hpgid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 hpgid.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
6 hpgid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 hpgid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8 colopp.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 colopp.p ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
10 colopp.1 ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
11 colhp.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
12 ancom ⊢ ( ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ∧ ¬ 𝐴 ∈ 𝐷 ) ↔ ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) )
13 12 a1i ⊢ ( 𝜑 → ( ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ∧ ¬ 𝐴 ∈ 𝐷 ) ↔ ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ) )
14 4 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
15 5 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
16 8 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐵 ∈ 𝑃 )
17 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
18 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
19 1 3 2 4 5 9 tglnpt ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
20 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 )
21 1 17 2 3 18 4 19 20 6 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝑃 )
22 21 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝑃 )
23 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐶 ∈ 𝐷 )
24 19 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐶 ∈ 𝑃 )
25 6 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 )
26 nelne2 ⊢ ( ( 𝐶 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐶 ≠ 𝐴 )
27 9 26 sylan ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐶 ≠ 𝐴 )
28 27 necomd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐴 ≠ 𝐶 )
29 1 17 2 3 18 4 19 20 6 mirbtwn ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) 𝐼 𝐴 ) )
30 1 17 2 4 21 19 6 29 tgbtwncom ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐶 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
32 1 2 3 14 25 24 22 28 31 btwnlng3 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ ( 𝐴 𝐿 𝐶 ) )
33 1 3 2 4 6 8 19 10 colrot1 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
34 1 3 2 4 8 19 6 33 colcom ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐴 ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
36 1 2 3 14 22 25 24 16 32 35 coltr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ ( 𝐶 𝐿 𝐵 ) ∨ 𝐶 = 𝐵 ) )
37 1 3 2 14 24 16 22 36 colrot1 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐶 ∈ ( 𝐵 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∨ 𝐵 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
38 1 2 3 14 15 16 7 22 23 37 colopp ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐵 𝑂 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ↔ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) ) )
39 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ¬ 𝐴 ∈ 𝐷 )
40 1 17 2 3 18 4 19 20 6 mirmir ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) = 𝐴 )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) = 𝐴 )
42 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
43 5 adantr ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
44 9 adantr ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → 𝐶 ∈ 𝐷 )
45 simpr ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 )
46 1 17 2 3 18 42 20 43 44 45 mirln ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∈ 𝐷 )
47 41 46 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
48 47 stoic1a ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑡 = 𝐶 ) → 𝑡 = 𝐶 )
50 49 eleq1d ⊢ ( ( 𝜑 ∧ 𝑡 = 𝐶 ) → ( 𝑡 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ↔ 𝐶 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ) )
51 9 50 30 rspcedvd ⊢ ( 𝜑 → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
53 39 48 52 jca31 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ) )
54 1 17 2 7 25 22 islnopp ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐴 𝑂 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ↔ ( ( ¬ 𝐴 ∈ 𝐷 ∧ ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ) ) )
55 53 54 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → 𝐴 𝑂 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) )
56 1 2 3 7 14 15 25 16 22 55 lnopp2hpgb ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐵 𝑂 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ↔ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) )
57 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐵 ∈ 𝑃 )
58 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐴 ∈ 𝑃 )
59 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐶 ∈ 𝑃 )
60 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐺 ∈ TarskiG )
61 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐶 ∈ 𝐷 )
62 simprr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → ¬ 𝐵 ∈ 𝐷 )
63 nelne2 ⊢ ( ( 𝐶 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) → 𝐶 ≠ 𝐵 )
64 63 necomd ⊢ ( ( 𝐶 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷 ) → 𝐵 ≠ 𝐶 )
65 61 62 64 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐵 ≠ 𝐶 )
66 28 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐴 ≠ 𝐶 )
67 simprl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
68 1 17 2 3 18 60 20 11 59 57 58 58 65 66 67 mirhl2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐵 ( 𝐾 ‘ 𝐶 ) 𝐴 )
69 1 2 11 57 58 59 60 68 hlcomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ) ) → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 )
70 69 3adantr3 ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) ) → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 )
71 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐴 ∈ 𝑃 )
72 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐵 ∈ 𝑃 )
73 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝑃 )
74 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐺 ∈ TarskiG )
75 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐶 ∈ 𝑃 )
76 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 )
77 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐶 ∈ ( 𝐴 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
78 1 2 11 71 72 73 74 75 76 77 btwnhl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) )
79 1 2 11 71 72 75 74 3 76 hlln ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
80 79 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) )
81 14 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐺 ∈ TarskiG )
82 16 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐵 ∈ 𝑃 )
83 75 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐶 ∈ 𝑃 )
84 25 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐴 ∈ 𝑃 )
85 76 adantr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 )
86 1 2 11 84 82 83 81 85 hlne2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐵 ≠ 𝐶 )
87 15 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐷 ∈ ran 𝐿 )
88 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐵 ∈ 𝐷 )
89 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐶 ∈ 𝐷 )
90 1 2 3 81 82 83 86 86 87 88 89 tglinethru ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐷 = ( 𝐵 𝐿 𝐶 ) )
91 80 90 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → 𝐴 ∈ 𝐷 )
92 39 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ∧ 𝐵 ∈ 𝐷 ) → ¬ 𝐴 ∈ 𝐷 )
93 91 92 pm2.65da ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → ¬ 𝐵 ∈ 𝐷 )
94 48 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 )
95 78 93 94 3jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) → ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) )
96 70 95 impbida ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( ( 𝐶 ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ) ∧ ¬ 𝐵 ∈ 𝐷 ∧ ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐶 ) ‘ 𝐴 ) ∈ 𝐷 ) ↔ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) )
97 38 56 96 3bitr3d ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ 𝐷 ) → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ↔ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) )
98 97 pm5.32da ⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ↔ ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ) ) )
99 simprr ⊢ ( ( 𝜑 ∧ ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ) → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )
100 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → 𝐺 ∈ TarskiG )
101 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → 𝐷 ∈ ran 𝐿 )
102 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → 𝐴 ∈ 𝑃 )
103 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → 𝐵 ∈ 𝑃 )
104 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )
105 1 2 3 7 100 101 102 103 104 hpgne1 ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → ¬ 𝐴 ∈ 𝐷 )
106 105 104 jca ⊢ ( ( 𝜑 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) → ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) )
107 99 106 impbida ⊢ ( 𝜑 → ( ( ¬ 𝐴 ∈ 𝐷 ∧ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) ↔ 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ) )
108 13 98 107 3bitr2rd ⊢ ( 𝜑 → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ↔ ( 𝐴 ( 𝐾 ‘ 𝐶 ) 𝐵 ∧ ¬ 𝐴 ∈ 𝐷 ) ) )