Metamath Proof Explorer

Theorem tgextalem1inag

Description: The point obtained by reflecting B through the midpoint of A and C lies inside the exterior angle <" A C D "> . Proved by Pasch on the midpoint and the extension, turned into an in-angle statement with isinagd and moved from ray C M to ray C A by inaghl . (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 tgextalem1inag ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ 𝒢 ∠ ⁡ G ⟨“ ACD ”⟩

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 eqid ⊢ pInv 𝒢 ⁡ G = pInv 𝒢 ⁡ G
15 1 4 3 6 8 9 7 12 ncolrot2 ⊢ φ → ¬ C ∈ A L B ∨ A = B
16 1 4 3 6 7 8 9 15 ncolcom ⊢ φ → ¬ C ∈ B L A ∨ B = A
17 1 4 3 6 8 7 9 16 ncolrot1 ⊢ φ → ¬ B ∈ A L C ∨ A = C
18 1 4 3 6 7 9 8 17 ncoltgdim2 ⊢ φ → G Dim 𝒢 ≥ 2
19 1 2 3 6 18 7 9 midcl ⊢ φ → A mid 𝒢 ⁡ G C ∈ P
20 eqid ⊢ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C = pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C
21 1 2 3 4 14 6 19 20 8 mircl ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
22 21 adantr ⊢ φ ∧ q ∈ P → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
23 22 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
24 19 adantr ⊢ φ ∧ q ∈ P → A mid 𝒢 ⁡ G C ∈ P
25 24 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A mid 𝒢 ⁡ G C ∈ P
26 9 adantr ⊢ φ ∧ q ∈ P → C ∈ P
27 26 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C ∈ P
28 10 adantr ⊢ φ ∧ q ∈ P → D ∈ P
29 28 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D ∈ P
30 6 adantr ⊢ φ ∧ q ∈ P → G ∈ 𝒢 Tarski
31 30 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → G ∈ 𝒢 Tarski
32 31 elexd ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → G ∈ V
33 simpl ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → φ ∧ q ∈ P
34 33 simprd ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → q ∈ P
35 ioran ⊢ ¬ B ∈ A L C ∨ A = C ↔ ¬ B ∈ A L C ∧ ¬ A = C
36 17 35 sylib ⊢ φ → ¬ B ∈ A L C ∧ ¬ A = C
37 36 simprd ⊢ φ → ¬ A = C
38 6 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → G ∈ 𝒢 Tarski
39 19 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → A mid 𝒢 ⁡ G C ∈ P
40 9 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → C ∈ P
41 7 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → A ∈ P
42 eqidd ⊢ φ → A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C
43 1 2 3 6 18 7 9 42 midcgr ⊢ φ → A mid 𝒢 ⁡ G C - ˙ A = A mid 𝒢 ⁡ G C - ˙ C
44 43 eqcomd ⊢ φ → A mid 𝒢 ⁡ G C - ˙ C = A mid 𝒢 ⁡ G C - ˙ A
45 44 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → A mid 𝒢 ⁡ G C - ˙ C = A mid 𝒢 ⁡ G C - ˙ A
46 simpr ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → A mid 𝒢 ⁡ G C = C
47 1 2 3 38 39 40 39 41 45 46 tgcgreq ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → A mid 𝒢 ⁡ G C = A
48 47 46 eqtr3d ⊢ φ ∧ A mid 𝒢 ⁡ G C = C → A = C
49 48 ex ⊢ φ → A mid 𝒢 ⁡ G C = C → A = C
50 49 necon3bd ⊢ φ → ¬ A = C → A mid 𝒢 ⁡ G C ≠ C
51 37 50 mpd ⊢ φ → A mid 𝒢 ⁡ G C ≠ C
52 51 adantr ⊢ φ ∧ q ∈ P → A mid 𝒢 ⁡ G C ≠ C
53 52 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → A mid 𝒢 ⁡ G C ≠ C
54 13 necomd ⊢ φ → D ≠ C
55 54 adantr ⊢ φ ∧ q ∈ P → D ≠ C
56 55 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → D ≠ C
57 1 2 3 6 7 19 axtgcgrrflx ⊢ φ → A - ˙ A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C - ˙ A
58 57 43 eqtrd ⊢ φ → A - ˙ A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C - ˙ C
59 1 2 3 6 9 19 axtgcgrrflx ⊢ φ → C - ˙ A mid 𝒢 ⁡ G C = A mid 𝒢 ⁡ G C - ˙ C
60 59 eqcomd ⊢ φ → A mid 𝒢 ⁡ G C - ˙ C = C - ˙ A mid 𝒢 ⁡ G C
61 58 60 eqtrd ⊢ φ → A - ˙ A mid 𝒢 ⁡ G C = C - ˙ A mid 𝒢 ⁡ G C
62 1 2 3 6 18 7 9 midbtwn ⊢ φ → A mid 𝒢 ⁡ G C ∈ A I C
63 1 2 3 4 14 6 19 20 8 mirbtwn ⊢ φ → A mid 𝒢 ⁡ G C ∈ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B I B
64 1 2 3 6 21 19 8 63 tgbtwncom ⊢ φ → A mid 𝒢 ⁡ G C ∈ B I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
65 simpr ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → A mid 𝒢 ⁡ G C = A
66 6 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → G ∈ 𝒢 Tarski
67 19 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → A mid 𝒢 ⁡ G C ∈ P
68 7 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → A ∈ P
69 9 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → C ∈ P
70 43 adantr ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → A mid 𝒢 ⁡ G C - ˙ A = A mid 𝒢 ⁡ G C - ˙ C
71 1 2 3 66 67 68 67 69 70 65 tgcgreq ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → A mid 𝒢 ⁡ G C = C
72 65 71 eqtr3d ⊢ φ ∧ A mid 𝒢 ⁡ G C = A → A = C
73 72 ex ⊢ φ → A mid 𝒢 ⁡ G C = A → A = C
74 73 necon3bd ⊢ φ → ¬ A = C → A mid 𝒢 ⁡ G C ≠ A
75 37 74 mpd ⊢ φ → A mid 𝒢 ⁡ G C ≠ A
76 37 neqned ⊢ φ → A ≠ C
77 1 3 4 6 7 9 19 76 62 btwnlng1 ⊢ φ → A mid 𝒢 ⁡ G C ∈ A L C
78 36 simpld ⊢ φ → ¬ B ∈ A L C
79 77 78 jca ⊢ φ → A mid 𝒢 ⁡ G C ∈ A L C ∧ ¬ B ∈ A L C
80 nelne2 ⊢ A mid 𝒢 ⁡ G C ∈ A L C ∧ ¬ B ∈ A L C → A mid 𝒢 ⁡ G C ≠ B
81 79 80 syl ⊢ φ → A mid 𝒢 ⁡ G C ≠ B
82 81 necomd ⊢ φ → B ≠ A mid 𝒢 ⁡ G C
83 1 2 3 4 14 6 19 20 8 82 mirne ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ≠ A mid 𝒢 ⁡ G C
84 83 necomd ⊢ φ → A mid 𝒢 ⁡ G C ≠ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
85 1 3 2 6 7 19 8 9 7 21 62 64 75 81 51 84 oacgr ⊢ φ → ⟨“ AA mid 𝒢 ⁡ G CB ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ CA mid 𝒢 ⁡ G C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ”⟩
86 1 2 3 4 14 6 19 20 8 mircgr ⊢ φ → A mid 𝒢 ⁡ G C - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B = A mid 𝒢 ⁡ G C - ˙ B
87 86 eqcomd ⊢ φ → A mid 𝒢 ⁡ G C - ˙ B = A mid 𝒢 ⁡ G C - ˙ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
88 1 3 4 6 7 8 9 12 ncolne1 ⊢ φ → A ≠ B
89 1 2 3 6 7 19 8 9 19 21 61 85 87 88 tgsas2 ⊢ φ → ⟨“ BAA mid 𝒢 ⁡ G C ”⟩ ∼ 𝒢 ∠ ⁡ G ⟨“ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B CA mid 𝒢 ⁡ G C ”⟩
90 1 3 5 6 8 7 19 21 9 19 89 cgrane3 ⊢ φ → C ≠ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
91 90 necomd ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ≠ C
92 91 adantr ⊢ φ ∧ q ∈ P → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ≠ C
93 92 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ≠ C
94 simpr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
95 94 simpld ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → q ∈ A mid 𝒢 ⁡ G C I D
96 27 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → C ∈ P
97 23 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ P
98 34 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → q ∈ P
99 31 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → G ∈ 𝒢 Tarski
100 94 simprd ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
101 100 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
102 93 necomd ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → C ≠ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
103 102 adantr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → C ≠ pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
104 simpr ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → ¬ q = C
105 104 neqned ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → q ≠ C
106 1 3 5 96 97 98 99 98 101 103 105 btwnhl1 ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∧ ¬ q = C → q K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
107 106 ex ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → ¬ q = C → q K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
108 107 orrd ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → q = C ∨ q K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
109 1 3 5 23 25 27 29 32 34 53 56 93 95 108 isinagd ⊢ φ ∧ q ∈ P ∧ q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ 𝒢 ∠ ⁡ G ⟨“ A mid 𝒢 ⁡ G CCD ”⟩
110 1 2 3 6 8 9 10 11 tgbtwncom ⊢ φ → C ∈ D I B
111 1 2 3 6 21 10 8 19 9 63 110 axtgpasch ⊢ φ → ∃ q ∈ P q ∈ A mid 𝒢 ⁡ G C I D ∧ q ∈ C I pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
112 109 111 r19.29a ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ 𝒢 ∠ ⁡ G ⟨“ A mid 𝒢 ⁡ G CCD ”⟩
113 1 3 5 7 9 19 6 10 62 76 51 btwnhl2 ⊢ φ → A mid 𝒢 ⁡ G C K ⁡ C A
114 1 3 5 19 7 9 6 113 hlcomd ⊢ φ → A K ⁡ C A mid 𝒢 ⁡ G C
115 1 3 5 10 10 9 6 54 hlid ⊢ φ → D K ⁡ C D
116 1 3 5 21 21 9 6 91 hlid ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B K ⁡ C pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B
117 1 3 5 21 19 9 10 6 112 7 10 21 114 115 116 inaghl ⊢ φ → pInv 𝒢 ⁡ G ⁡ A mid 𝒢 ⁡ G C ⁡ B ∈ 𝒢 ∠ ⁡ G ⟨“ ACD ”⟩