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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgextalem1inag.m ⊢ − = ( dist ‘ 𝐺 )
tgextalem1inag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgextalem1inag.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgextalem1inag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
tgextalem1inag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgextalem1inag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgextalem1inag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgextalem1inag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgextalem1inag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgextalem1inag.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
tgextalem1inag.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
tgextalem1inag.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
Assertion tgextalem1inag ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgextalem1inag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgextalem1inag.m ⊢ − = ( dist ‘ 𝐺 )
3 tgextalem1inag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgextalem1inag.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgextalem1inag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 tgextalem1inag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 tgextalem1inag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 tgextalem1inag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 tgextalem1inag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 tgextalem1inag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11 tgextalem1inag.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12 tgextalem1inag.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
13 tgextalem1inag.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
14 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
15 1 4 3 6 8 9 7 12 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
16 1 4 3 6 7 8 9 15 ncolcom ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
17 1 4 3 6 8 7 9 16 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
18 1 4 3 6 7 9 8 17 ncoltgdim2 ⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
19 1 2 3 6 18 7 9 midcl ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
20 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
21 1 2 3 4 14 6 19 20 8 mircl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
22 21 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
24 19 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
26 9 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → 𝐶 ∈ 𝑃 )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝐶 ∈ 𝑃 )
28 10 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → 𝐷 ∈ 𝑃 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝐷 ∈ 𝑃 )
30 6 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝐺 ∈ TarskiG )
32 31 elexd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝐺 ∈ V )
33 simpl ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) )
34 33 simprd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝑞 ∈ 𝑃 )
35 ioran ⊢ ( ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) ↔ ( ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝐴 = 𝐶 ) )
36 17 35 sylib ⊢ ( 𝜑 → ( ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝐴 = 𝐶 ) )
37 36 simprd ⊢ ( 𝜑 → ¬ 𝐴 = 𝐶 )
38 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → 𝐺 ∈ TarskiG )
39 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
40 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → 𝐶 ∈ 𝑃 )
41 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → 𝐴 ∈ 𝑃 )
42 eqidd ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
43 1 2 3 6 18 7 9 42 midcgr ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐴 ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) )
44 43 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐴 ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐴 ) )
46 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 )
47 1 2 3 38 39 40 39 41 45 46 tgcgreq ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 )
48 47 46 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 ) → 𝐴 = 𝐶 )
49 48 ex ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 → 𝐴 = 𝐶 ) )
50 49 necon3bd ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐶 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐶 ) )
51 37 50 mpd ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐶 )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐶 )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐶 )
54 13 necomd ⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → 𝐷 ≠ 𝐶 )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝐷 ≠ 𝐶 )
57 1 2 3 6 7 19 axtgcgrrflx ⊢ ( 𝜑 → ( 𝐴 − ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐴 ) )
58 57 43 eqtrd ⊢ ( 𝜑 → ( 𝐴 − ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) )
59 1 2 3 6 9 19 axtgcgrrflx ⊢ ( 𝜑 → ( 𝐶 − ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) )
60 59 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) = ( 𝐶 − ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
61 58 60 eqtrd ⊢ ( 𝜑 → ( 𝐴 − ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( 𝐶 − ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) )
62 1 2 3 6 18 7 9 midbtwn ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐼 𝐶 ) )
63 1 2 3 4 14 6 19 20 8 mirbtwn ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) 𝐼 𝐵 ) )
64 1 2 3 6 21 19 8 63 tgbtwncom ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐵 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
65 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 )
66 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → 𝐺 ∈ TarskiG )
67 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
68 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → 𝐴 ∈ 𝑃 )
69 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → 𝐶 ∈ 𝑃 )
70 43 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐴 ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐶 ) )
71 1 2 3 66 67 68 67 69 70 65 tgcgreq ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐶 )
72 65 71 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 ) → 𝐴 = 𝐶 )
73 72 ex ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) = 𝐴 → 𝐴 = 𝐶 ) )
74 73 necon3bd ⊢ ( 𝜑 → ( ¬ 𝐴 = 𝐶 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐴 ) )
75 37 74 mpd ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐴 )
76 37 neqned ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
77 1 3 4 6 7 9 19 76 62 btwnlng1 ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐿 𝐶 ) )
78 36 simpld ⊢ ( 𝜑 → ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) )
79 77 78 jca ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ) )
80 nelne2 ⊢ ( ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ ( 𝐴 𝐿 𝐶 ) ∧ ¬ 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐵 )
81 79 80 syl ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ 𝐵 )
82 81 necomd ⊢ ( 𝜑 → 𝐵 ≠ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
83 1 2 3 4 14 6 19 20 8 82 mirne ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ≠ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
84 83 necomd ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
85 1 3 2 6 7 19 8 9 7 21 62 64 75 81 51 84 oacgr ⊢ ( 𝜑 → ⟨“ 𝐴 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )
86 1 2 3 4 14 6 19 20 8 mircgr ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐵 ) )
87 86 eqcomd ⊢ ( 𝜑 → ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − 𝐵 ) = ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) − ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
88 1 3 4 6 7 8 9 12 ncolne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
89 1 2 3 6 7 19 8 9 19 21 61 85 87 88 tgsas2 ⊢ ( 𝜑 → ⟨“ 𝐵 𝐴 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) 𝐶 ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ”⟩ )
90 1 3 5 6 8 7 19 21 9 19 89 cgrane3 ⊢ ( 𝜑 → 𝐶 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
91 90 necomd ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ≠ 𝐶 )
92 91 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ≠ 𝐶 )
93 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ≠ 𝐶 )
94 simpr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) )
95 94 simpld ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) )
96 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝐶 ∈ 𝑃 )
97 23 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
98 34 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝑞 ∈ 𝑃 )
99 31 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝐺 ∈ TarskiG )
100 94 simprd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
101 100 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
102 93 necomd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → 𝐶 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
103 102 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝐶 ≠ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
104 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → ¬ 𝑞 = 𝐶 )
105 104 neqned ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝑞 ≠ 𝐶 )
106 1 3 5 96 97 98 99 98 101 103 105 btwnhl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ∧ ¬ 𝑞 = 𝐶 ) → 𝑞 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
107 106 ex ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( ¬ 𝑞 = 𝐶 → 𝑞 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
108 107 orrd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( 𝑞 = 𝐶 ∨ 𝑞 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
109 1 3 5 23 25 27 29 32 34 53 56 93 95 108 isinagd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐶 𝐷 ”⟩ )
110 1 2 3 6 8 9 10 11 tgbtwncom ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐷 𝐼 𝐵 ) )
111 1 2 3 6 21 10 8 19 9 63 110 axtgpasch ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝑃 ( 𝑞 ∈ ( ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐼 𝐷 ) ∧ 𝑞 ∈ ( 𝐶 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) )
112 109 111 r19.29a ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) 𝐶 𝐷 ”⟩ )
113 1 3 5 7 9 19 6 10 62 76 51 btwnhl2 ⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ( 𝐾 ‘ 𝐶 ) 𝐴 )
114 1 3 5 19 7 9 6 113 hlcomd ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐶 ) ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
115 1 3 5 10 10 9 6 54 hlid ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐶 ) 𝐷 )
116 1 3 5 21 21 9 6 91 hlid ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
117 1 3 5 21 19 9 10 6 112 7 10 21 114 115 116 inaghl ⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )