tgextalem1inag - Mathbox for Jorge Agra

	Mathbox for Jorge Agra		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > tgextalem1inag		Structured version Visualization version GIF version

Theorem tgextalem1inag 33070

Description: The point obtained by reflecting 𝐵 through the midpoint of 𝐴 and 𝐶 lies inside the exterior angle ⟨“𝐴𝐶𝐷”⟩. Proved by Pasch on the midpoint and the extension, turned into an in-angle statement with isinagd 29358 and moved from ray 𝐶𝑀 to ray 𝐶𝐴 by inaghl 29364. (Contributed by JAG, 12-Aug-2026.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
tgextalem1inag	⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)(inA‘𝐺)⟨“𝐴𝐶𝐷”⟩)

Proof of Theorem tgextalem1inag Dummy variable 𝑞 is distinct from all other variables.

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 Vcvv 3450 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ⟨“cs3 14993 Basecbs 17387 distcds 17437 TarskiGcstrkg 28889 Itvcitv 28895 LineGclng 28896 hlGchlg 29063 pInvGcmir 29124 midGcmid 29277 inAcinag 29354

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-oadd 8480 df-er 8717 df-map 8849 df-pm 8850 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-dju 9982 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-xnn0 12680 df-z 12694 df-uz 12966 df-fz 13640 df-fzo 13789 df-hash 14475 df-word 14659 df-concat 14716 df-s1 14743 df-s2 14999 df-s3 15000 df-trkgc 28910 df-trkgb 28911 df-trkgcb 28912 df-trkgld 28914 df-trkg 28915 df-cgrg 28974 df-leg 29046 df-hlg 29064 df-mir 29125 df-rag 29169 df-perpg 29171 df-mid 29279 df-cgra 29315 df-inag 29356

This theorem is used by: tgextale 33071 tgextahp 33073

W3C validator