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 33100

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 29388 and moved from ray 𝐶𝑀 to ray 𝐶𝐴 by inaghl 29394. (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 2763	. . 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 29056	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵))
13	1, 5, 2, 7, 8, 10, 9, 12	ncolcom 29054	. . . . . 6 ⊢ (𝜑 → ¬ (𝐶 ∈ (𝐵𝐿𝐴) ∨ 𝐵 = 𝐴))
14	1, 5, 2, 7, 10, 8, 9, 13	ncolrot1 29055	. . . . 5 ⊢ (𝜑 → ¬ (𝐵 ∈ (𝐴𝐿𝐶) ∨ 𝐴 = 𝐶))
15	1, 5, 2, 7, 8, 9, 10, 14	ncoltgdim2 29058	. . . 4 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
16	1, 4, 2, 7, 15, 8, 9	midcl 29312	. . 3 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
17		eqid 2763	. . 3 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
18	1, 4, 2, 5, 6, 7, 16, 17, 10	mircl 29163	. 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 3477	. . . 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 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
41	1, 4, 2, 7, 15, 8, 9, 40	midcgr 29315	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) − 𝐴) = ((𝐴(midG‘𝐺)𝐶) − 𝐶))
42	41	eqcomd 2769	. . . . . . . . . . . 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 28974	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐶) = 𝐶) → (𝐴(midG‘𝐺)𝐶) = 𝐴)
46	45, 44	eqtr3d 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐶) = 𝐶) → 𝐴 = 𝐶)
47	46	ex 418	. . . . . . . 8 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) = 𝐶 → 𝐴 = 𝐶))
48	47	necon3bd 2973	. . . . . . 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 3014	. . . . . 6 ⊢ (𝜑 → 𝐷 ≠ 𝐶)
54	53	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑞 ∈ 𝑃) → 𝐷 ≠ 𝐶)
55	54	adantr 486	. . . 4 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑃) ∧ (𝑞 ∈ ((𝐴(midG‘𝐺)𝐶)𝐼𝐷) ∧ 𝑞 ∈ (𝐶𝐼(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)))) → 𝐷 ≠ 𝐶)
56	1, 4, 2, 7, 8, 16	axtgcgrrflx 28954	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 − (𝐴(midG‘𝐺)𝐶)) = ((𝐴(midG‘𝐺)𝐶) − 𝐴))
57	56, 41	eqtrd 2798	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 − (𝐴(midG‘𝐺)𝐶)) = ((𝐴(midG‘𝐺)𝐶) − 𝐶))
58	1, 4, 2, 7, 9, 16	axtgcgrrflx 28954	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 − (𝐴(midG‘𝐺)𝐶)) = ((𝐴(midG‘𝐺)𝐶) − 𝐶))
59	58	eqcomd 2769	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) − 𝐶) = (𝐶 − (𝐴(midG‘𝐺)𝐶)))
60	57, 59	eqtrd 2798	. . . . . . . . 9 ⊢ (𝜑 → (𝐴 − (𝐴(midG‘𝐺)𝐶)) = (𝐶 − (𝐴(midG‘𝐺)𝐶)))
61	1, 4, 2, 7, 15, 8, 9	midbtwn 29314	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ (𝐴𝐼𝐶))
62	1, 4, 2, 5, 6, 7, 16, 17, 10	mirbtwn 29160	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ ((((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)𝐼𝐵))
63	1, 4, 2, 7, 18, 16, 10, 62	tgbtwncom 28981	. . . . . . . . . 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 28974	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐶) = 𝐴) → (𝐴(midG‘𝐺)𝐶) = 𝐶)
71	64, 70	eqtr3d 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐴(midG‘𝐺)𝐶) = 𝐴) → 𝐴 = 𝐶)
72	71	ex 418	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) = 𝐴 → 𝐴 = 𝐶))
73	72	necon3bd 2973	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝐴 = 𝐶 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐴))
74	35, 73	mpd 16	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐴)
75	35	neqned 2966	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
76	1, 2, 5, 7, 8, 9, 16, 75, 61	btwnlng1 29117	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ (𝐴𝐿𝐶))
77	34	simpld 500	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝐵 ∈ (𝐴𝐿𝐶))
78	76, 77	jca 521	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) ∈ (𝐴𝐿𝐶) ∧ ¬ 𝐵 ∈ (𝐴𝐿𝐶)))
79		nelne2 3057	. . . . . . . . . . 11 ⊢ (((𝐴(midG‘𝐺)𝐶) ∈ (𝐴𝐿𝐶) ∧ ¬ 𝐵 ∈ (𝐴𝐿𝐶)) → (𝐴(midG‘𝐺)𝐶) ≠ 𝐵)
80	78, 79	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐵)
81	80	necomd 3014	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ≠ (𝐴(midG‘𝐺)𝐶))
82	1, 4, 2, 5, 6, 7, 16, 17, 10, 81	mirne 29169	. . . . . . . . . . 11 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ≠ (𝐴(midG‘𝐺)𝐶))
83	82	necomd 3014	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))
84	1, 2, 4, 7, 8, 16, 10, 9, 8, 18, 61, 63, 74, 80, 49, 83	oacgr 29370	. . . . . . . . 9 ⊢ (𝜑 → ⟨“𝐴(𝐴(midG‘𝐺)𝐶)𝐵”⟩(cgrA‘𝐺)⟨“𝐶(𝐴(midG‘𝐺)𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)”⟩)
85	1, 4, 2, 5, 6, 7, 16, 17, 10	mircgr 29159	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) = ((𝐴(midG‘𝐺)𝐶) − 𝐵))
86	85	eqcomd 2769	. . . . . . . . 9 ⊢ (𝜑 → ((𝐴(midG‘𝐺)𝐶) − 𝐵) = ((𝐴(midG‘𝐺)𝐶) − (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)))
87	1, 2, 5, 7, 8, 10, 9, 11	ncolne1 29123	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
88	1, 4, 2, 7, 8, 16, 10, 9, 16, 18, 60, 84, 86, 87	tgsas2 29431	. . . . . . . 8 ⊢ (𝜑 → ⟨“𝐵𝐴(𝐴(midG‘𝐺)𝐶)”⟩(cgrA‘𝐺)⟨“(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)𝐶(𝐴(midG‘𝐺)𝐶)”⟩)
89	1, 2, 3, 7, 10, 8, 16, 18, 9, 16, 88	cgrane3 29351	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))
90	89	necomd 3014	. . . . . 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 3014	. . . . . . . 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 2966	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑞 ∈ 𝑃) ∧ (𝑞 ∈ ((𝐴(midG‘𝐺)𝐶)𝐼𝐷) ∧ 𝑞 ∈ (𝐶𝐼(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)))) ∧ ¬ 𝑞 = 𝐶) → 𝑞 ≠ 𝐶)
105	1, 2, 3, 95, 96, 97, 98, 97, 100, 102, 104	btwnhl1 29108	. . . . . 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 29388	. . 3 ⊢ (((𝜑 ∧ 𝑞 ∈ 𝑃) ∧ (𝑞 ∈ ((𝐴(midG‘𝐺)𝐶)𝐼𝐷) ∧ 𝑞 ∈ (𝐶𝐼(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)))) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)(inA‘𝐺)⟨“(𝐴(midG‘𝐺)𝐶)𝐶𝐷”⟩)
109		tgextalem1inag.ext	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))
110	1, 4, 2, 7, 10, 9, 19, 109	tgbtwncom 28981	. . . 4 ⊢ (𝜑 → 𝐶 ∈ (𝐷𝐼𝐵))
111	1, 4, 2, 7, 18, 19, 10, 16, 9, 62, 110	axtgpasch 28959	. . 3 ⊢ (𝜑 → ∃𝑞 ∈ 𝑃 (𝑞 ∈ ((𝐴(midG‘𝐺)𝐶)𝐼𝐷) ∧ 𝑞 ∈ (𝐶𝐼(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))))
112	108, 111	r19.29a 3174	. 2 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)(inA‘𝐺)⟨“(𝐴(midG‘𝐺)𝐶)𝐶𝐷”⟩)
113	1, 2, 3, 8, 9, 16, 7, 19, 61, 75, 49	btwnhl2 29109	. . 3 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶)(𝐾‘𝐶)𝐴)
114	1, 2, 3, 16, 8, 9, 7, 113	hlcomd 29100	. 2 ⊢ (𝜑 → 𝐴(𝐾‘𝐶)(𝐴(midG‘𝐺)𝐶))
115	1, 2, 3, 19, 19, 9, 7, 53	hlid 29105	. 2 ⊢ (𝜑 → 𝐷(𝐾‘𝐶)𝐷)
116	1, 2, 3, 18, 18, 9, 7, 90	hlid 29105	. 2 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))
117	1, 2, 3, 18, 16, 9, 19, 7, 112, 8, 19, 18, 114, 115, 116	inaghl 29394	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 1570 ∈ wcel 2147 ≠ wne 2959 Vcvv 3454 class class class wbr 5106 ‘cfv 6558 (class class class)co 7443 ⟨“cs3 15021 Basecbs 17416 distcds 17466 TarskiGcstrkg 28919 Itvcitv 28925 LineGclng 28926 hlGchlg 29093 pInvGcmir 29154 midGcmid 29307 inAcinag 29384

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-oadd 8508 df-er 8745 df-map 8877 df-pm 8878 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-dju 10009 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-2 12432 df-3 12433 df-n0 12634 df-xnn0 12707 df-z 12721 df-uz 12993 df-fz 13667 df-fzo 13816 df-hash 14502 df-word 14686 df-concat 14743 df-s1 14770 df-s2 15027 df-s3 15028 df-trkgc 28940 df-trkgb 28941 df-trkgcb 28942 df-trkgld 28944 df-trkg 28945 df-cgrg 29004 df-leg 29076 df-hlg 29094 df-mir 29155 df-rag 29199 df-perpg 29201 df-mid 29309 df-cgra 29345 df-inag 29386

This theorem is used by: tgextale 33101 tgextahp 33103

W3C validator