Metamath Proof Explorer

Theorem tgextahp

Description: The reflected point and D lie on the same OPEN half-plane of line A C -- the fact acopyeu requires and inA does not give. tgextalem1inag puts the reflected point inside the exterior angle, which is non-strict: isinag 's witness clause is ( x = C \/ x ( KC ) P ) , so a point inside an angle may sit on a boundary ray. The x = C branch collapses to ( A e. ( C L D ) \/ C = D ) and is killed by tgextancd ; the main branch is tgextahpl , whose off-line input is tgextamirn . The $d s are the mandatory ones isinag carries for the witness variable. (Contributed by JAG , 12-Aug-2026)

Ref Expression
Hypotheses tgextalem1inag.p ⊢ P = Base G
tgextalem1inag.m ⊢ - ˙ = dist ⁡ G
tgextalem1inag.i ⊢ I = Itv ⁡ G
tgextalem1inag.l ⊢ L = Line 𝒢 ⁡ G
tgextalem1inag.k ⊢ K = hl 𝒢 ⁡ G
tgextalem1inag.g ⊢ φ → G ∈ 𝒢 Tarski
tgextalem1inag.a ⊢ φ → A ∈ P
tgextalem1inag.b ⊢ φ → B ∈ P
tgextalem1inag.c ⊢ φ → C ∈ P
tgextalem1inag.d ⊢ φ → D ∈ P
tgextalem1inag.ext ⊢ φ → C ∈ B I D
tgextalem1inag.ncol ⊢ φ → ¬ A ∈ B L C ∨ B = C
tgextalem1inag.ne ⊢ φ → C ≠ D
Assertion tgextahp ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B hp 𝒢 ⁡ G ⁡ A L C D

Proof

Step Hyp Ref Expression
1 tgextalem1inag.p ⊢ P = Base G
2 tgextalem1inag.m ⊢ - ˙ = dist ⁡ G
3 tgextalem1inag.i ⊢ I = Itv ⁡ G
4 tgextalem1inag.l ⊢ L = Line 𝒢 ⁡ G
5 tgextalem1inag.k ⊢ K = hl 𝒢 ⁡ G
6 tgextalem1inag.g ⊢ φ → G ∈ 𝒢 Tarski
7 tgextalem1inag.a ⊢ φ → A ∈ P
8 tgextalem1inag.b ⊢ φ → B ∈ P
9 tgextalem1inag.c ⊢ φ → C ∈ P
10 tgextalem1inag.d ⊢ φ → D ∈ P
11 tgextalem1inag.ext ⊢ φ → C ∈ B I D
12 tgextalem1inag.ncol ⊢ φ → ¬ A ∈ B L C ∨ B = C
13 tgextalem1inag.ne ⊢ φ → C ≠ D
14 1 2 3 4 5 6 7 8 9 10 11 12 13 tgextalem1inag ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ 𝒢 ∠ ⁡ G ⟨“ ACD ”⟩
15 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
16 1 4 3 6 8 9 7 12 ncoltgdim2 ⊢ φ → G Dim 𝒢 ≥ 2
17 1 2 3 6 16 7 9 midcl ⊢ φ → A mid 𝒢 ⁡ G C ∈ P
18 eqid ⊢ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C
19 1 2 3 4 15 6 17 18 8 mircl ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
20 1 3 5 19 7 9 10 6 isinag ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ 𝒢 ∠ ⁡ G ⟨“ ACD ”⟩ ↔ A ≠ C ∧ D ≠ C ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ≠ C ∧ ∃ x ∈ P x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
21 14 20 mpbid ⊢ φ → A ≠ C ∧ D ≠ C ∧ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ≠ C ∧ ∃ x ∈ P x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
22 21 simprd ⊢ φ → ∃ x ∈ P x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
23 6 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → G ∈ 𝒢 Tarski
24 23 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → G ∈ 𝒢 Tarski
25 9 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C ∈ P
26 25 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → C ∈ P
27 10 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D ∈ P
28 27 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → D ∈ P
29 7 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A ∈ P
30 29 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → A ∈ P
31 simpr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → x = C
32 simprrl ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → x ∈ A I D
33 32 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → x ∈ A I D
34 31 33 eqeltrrd ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → C ∈ A I D
35 1 4 3 24 26 28 30 34 btwncolg2 ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → A ∈ C L D ∨ C = D
36 1 2 3 4 6 7 8 9 10 11 12 13 tgextancd ⊢ φ → ¬ A ∈ C L D ∨ C = D
37 36 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → ¬ A ∈ C L D ∨ C = D
38 37 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → ¬ A ∈ C L D ∨ C = D
39 35 38 pm2.21dd ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x = C → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B hp 𝒢 ⁡ G ⁡ A L C D
40 23 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → G ∈ 𝒢 Tarski
41 29 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A ∈ P
42 25 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C ∈ P
43 27 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D ∈ P
44 19 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
45 44 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
46 simprl ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → x ∈ P
47 46 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → x ∈ P
48 37 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → ¬ A ∈ C L D ∨ C = D
49 1 2 3 4 6 7 8 9 12 tgextamirn ⊢ φ → ¬ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C
50 49 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → ¬ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C
51 50 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → ¬ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ A L C
52 32 adantr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → x ∈ A I D
53 simpr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
54 1 2 3 4 5 40 41 42 43 45 47 48 51 52 53 tgextahpl ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B hp 𝒢 ⁡ G ⁡ A L C D
55 simprrr ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
56 39 54 55 mpjaodan ⊢ φ ∧ x ∈ P ∧ x ∈ A I D ∧ x = C ∨ x K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B hp 𝒢 ⁡ G ⁡ A L C D
57 22 56 rexlimddv ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B hp 𝒢 ⁡ G ⁡ A L C D