tgextamirnhl - Mathbox for Jorge Agra

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

Theorem tgextamirnhl 33102

Description: The midpoint-reflected point is not on the ray from 𝐶 through 𝐷. If it were, then -- ray 𝐶𝐷 being the extension of 𝐵𝐶-- it would lie on line 𝐶𝐵; mirln2 29179, the converse of the mirln 29178 used in tgextamirn 33097, would put the midpoint of 𝐴 and 𝐶 on that line too; and the midpoint is collinear with 𝐴 and 𝐶, so 𝐴 would land on line 𝐶𝐵, contradicting the triangle's non-collinearity. 𝑀 ≠ 𝐶 comes from ismidb 29313 / mirinv 29168 / mirne 29169, not from midbtwn 29314. (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
tgextamirnhl	⊢ (𝜑 → ¬ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))

**Proof of Theorem tgextamirnhl**
Step	Hyp	Ref	Expression
1		tgextalem1inag.p	. . . . 5 ⊢ 𝑃 = (Base‘𝐺)
2		tgextalem1inag.l	. . . . 5 ⊢ 𝐿 = (LineG‘𝐺)
3		tgextalem1inag.i	. . . . 5 ⊢ 𝐼 = (Itv‘𝐺)
4		tgextalem1inag.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5		tgextalem1inag.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
6		tgextalem1inag.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
7		tgextalem1inag.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
8		tgextalem1inag.ncol	. . . . 5 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐵𝐿𝐶) ∨ 𝐵 = 𝐶))
9	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29054	. . . 4 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
10		ioran 999	. . . 4 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
11	9, 10	sylib 221	. . 3 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
12	11	simpld 500	. 2 ⊢ (𝜑 → ¬ 𝐴 ∈ (𝐶𝐿𝐵))
13	4	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
14	6	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ∈ 𝑃)
15		tgextalem1inag.m	. . . . . . 7 ⊢ − = (dist‘𝐺)
16	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . 7 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
17	1, 15, 3, 4, 16, 7, 6	midcl 29312	. . . . . 6 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
18	17	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
19	7	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐴 ∈ 𝑃)
20	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . 8 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
21	1, 15, 3, 4, 20, 7, 6	midcl 29312	. . . . . . 7 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
22	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . 8 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
23	1, 15, 3, 4, 22, 7, 6	midbtwn 29314	. . . . . . 7 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ (𝐴𝐼𝐶))
24	1, 15, 3, 4, 7, 21, 6, 23	tgbtwncom 28981	. . . . . 6 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ (𝐶𝐼𝐴))
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ (𝐶𝐼𝐴))
26	1, 2, 3, 13, 14, 18, 19, 25	btwncolg3 29050	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴 ∈ (𝐶𝐿(𝐴(midG‘𝐺)𝐶)) ∨ 𝐶 = (𝐴(midG‘𝐺)𝐶)))
27		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
28	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
29		eqid 2763	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
30	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31	1, 15, 3, 4, 30, 7, 6	midcl 29312	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
32	1, 15, 3, 4, 28, 7, 6, 29, 31	ismidb 29313	. . . . . . . 8 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
33	27, 32	mpbird 260	. . . . . . 7 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
34		eqid 2763	. . . . . . . 8 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
35	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
36	1, 15, 3, 4, 35, 7, 6	midcl 29312	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
37		eqid 2763	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
38	1, 3, 2, 4, 7, 5, 6, 8	ncolne2 29124	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
39	38	necomd 3014	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐴)
40		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
41	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
42		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
43	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
44	1, 15, 3, 4, 43, 7, 6	midcl 29312	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
45	1, 15, 3, 4, 41, 7, 6, 42, 44	ismidb 29313	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
46	40, 45	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
47	46	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴))
48		eqid 2763	. . . . . . . . . . . . 13 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
49	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
50	1, 15, 3, 4, 49, 7, 6	midcl 29312	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
51		eqid 2763	. . . . . . . . . . . . 13 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
52	1, 15, 3, 2, 48, 4, 50, 51, 7	mirinv 29168	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
53	47, 52	bitrd 282	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
54	53	necon3bid 3003	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) ≠ 𝐴))
55	39, 54	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐴)
56	55	necomd 3014	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ (𝐴(midG‘𝐺)𝐶))
57	1, 15, 3, 2, 34, 4, 36, 37, 7, 56	mirne 29169	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ≠ (𝐴(midG‘𝐺)𝐶))
58	33, 57	eqnetrd 3026	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ (𝐴(midG‘𝐺)𝐶))
59	58	neneqd 2964	. . . . 5 ⊢ (𝜑 → ¬ 𝐶 = (𝐴(midG‘𝐺)𝐶))
60	59	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → ¬ 𝐶 = (𝐴(midG‘𝐺)𝐶))
61	26, 60	olcnd 891	. . 3 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐴 ∈ (𝐶𝐿(𝐴(midG‘𝐺)𝐶)))
62	4	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
63	6	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ∈ 𝑃)
64	5	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐵 ∈ 𝑃)
65	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29054	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
66		ioran 999	. . . . . . . 8 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
67	65, 66	sylib 221	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
68	67	simprd 501	. . . . . 6 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
69	68	neqned 2966	. . . . 5 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
70	69	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ≠ 𝐵)
71	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . 6 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
72	1, 15, 3, 4, 71, 7, 6	midcl 29312	. . . . 5 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
73	72	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
74		eqidd 2764	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
75	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
76		eqid 2763	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
77	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
78	1, 15, 3, 4, 77, 7, 6	midcl 29312	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
79	1, 15, 3, 4, 75, 7, 6, 76, 78	ismidb 29313	. . . . . . . 8 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
80	74, 79	mpbird 260	. . . . . . 7 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
81		eqid 2763	. . . . . . . 8 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
82	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
83	1, 15, 3, 4, 82, 7, 6	midcl 29312	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
84		eqid 2763	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
85	1, 3, 2, 4, 7, 5, 6, 8	ncolne2 29124	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
86	85	necomd 3014	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐴)
87		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
88	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
89		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
90	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
91	1, 15, 3, 4, 90, 7, 6	midcl 29312	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
92	1, 15, 3, 4, 88, 7, 6, 89, 91	ismidb 29313	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
93	87, 92	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
94	93	eqeq1d 2765	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴))
95		eqid 2763	. . . . . . . . . . . . 13 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
96	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
97	1, 15, 3, 4, 96, 7, 6	midcl 29312	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
98		eqid 2763	. . . . . . . . . . . . 13 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
99	1, 15, 3, 2, 95, 4, 97, 98, 7	mirinv 29168	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
100	94, 99	bitrd 282	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
101	100	necon3bid 3003	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) ≠ 𝐴))
102	86, 101	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐴)
103	102	necomd 3014	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ (𝐴(midG‘𝐺)𝐶))
104	1, 15, 3, 2, 81, 4, 83, 84, 7, 103	mirne 29169	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ≠ (𝐴(midG‘𝐺)𝐶))
105	80, 104	eqnetrd 3026	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ (𝐴(midG‘𝐺)𝐶))
106	105	necomd 3014	. . . . 5 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐶)
107	106	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ≠ 𝐶)
108		eqid 2763	. . . . 5 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
109	4	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
110		eqid 2763	. . . . 5 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
111	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29054	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
112		ioran 999	. . . . . . . . . 10 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
113	111, 112	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
114	113	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
115	114	neqned 2966	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
116	1, 3, 2, 4, 6, 5, 115	tgelrnln 29128	. . . . . 6 ⊢ (𝜑 → (𝐶𝐿𝐵) ∈ ran 𝐿)
117	116	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐶𝐿𝐵) ∈ ran 𝐿)
118	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . 7 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
119	1, 15, 3, 4, 118, 7, 6	midcl 29312	. . . . . 6 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
120	119	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
121	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29054	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
122		ioran 999	. . . . . . . . . 10 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
123	121, 122	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
124	123	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
125	124	neqned 2966	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
126	1, 3, 2, 4, 6, 5, 125	tglinerflx2 29132	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐿𝐵))
127	126	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐵 ∈ (𝐶𝐿𝐵))
128		tgextalem1inag.k	. . . . . . . 8 ⊢ 𝐾 = (hlG‘𝐺)
129		eqid 2763	. . . . . . . . . 10 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
130	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
131	1, 15, 3, 4, 130, 7, 6	midcl 29312	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
132		eqid 2763	. . . . . . . . . 10 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
133	1, 15, 3, 2, 129, 4, 131, 132, 5	mircl 29163	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ 𝑃)
134	133	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ 𝑃)
135		tgextalem1inag.d	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
136	135	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐷 ∈ 𝑃)
137	6	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ∈ 𝑃)
138	4	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
139	135	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐷 ∈ 𝑃)
140		eqid 2763	. . . . . . . . . . 11 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
141	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29058	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
142	1, 15, 3, 4, 141, 7, 6	midcl 29312	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
143		eqid 2763	. . . . . . . . . . 11 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
144	1, 15, 3, 2, 140, 4, 142, 143, 5	mircl 29163	. . . . . . . . . 10 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ 𝑃)
145	144	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ 𝑃)
146	6	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ∈ 𝑃)
147	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
148		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))
149	1, 3, 128, 139, 145, 146, 147, 148	hlcomd 29100	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)(𝐾‘𝐶)𝐷)
150	1, 3, 128, 134, 136, 137, 138, 2, 149	hlln 29103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ (𝐷𝐿𝐶))
151	4	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
152	135	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐷 ∈ 𝑃)
153	6	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ∈ 𝑃)
154		tgextalem1inag.ne	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
155	154	necomd 3014	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐶)
156	155	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐷 ≠ 𝐶)
157	1, 3, 2, 151, 152, 153, 156	tglinecom 29133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐷𝐿𝐶) = (𝐶𝐿𝐷))
158	150, 157	eleqtrd 2866	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ (𝐶𝐿𝐷))
159	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29054	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
160		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
161	159, 160	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
162	161	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
163	162	neqned 2966	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
164	154	necomd 3014	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ≠ 𝐶)
165		tgextalem1inag.ext	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))
166	1, 15, 3, 4, 5, 6, 135, 165	tgbtwncom 28981	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ (𝐷𝐼𝐵))
167	1, 2, 3, 4, 6, 5, 135, 166	btwncolg2 29049	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
168	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29054	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
169		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
170	168, 169	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
171	170	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
172	167, 171	olcnd 891	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ (𝐶𝐿𝐵))
173	1, 3, 2, 4, 6, 5, 163, 135, 164, 172	tglineelsb2 29130	. . . . . . 7 ⊢ (𝜑 → (𝐶𝐿𝐵) = (𝐶𝐿𝐷))
174	173	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐶𝐿𝐵) = (𝐶𝐿𝐷))
175	158, 174	eleqtrrd 2867	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ (𝐶𝐿𝐵))
176	1, 15, 3, 2, 108, 109, 110, 117, 120, 127, 175	mirln2 29179	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ (𝐶𝐿𝐵))
177	1, 3, 2, 62, 63, 64, 70, 73, 107, 176	tglineelsb2 29130	. . 3 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐶𝐿𝐵) = (𝐶𝐿(𝐴(midG‘𝐺)𝐶)))
178	61, 177	eleqtrrd 2867	. 2 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐴 ∈ (𝐶𝐿𝐵))
179	12, 178	mtand 828	1 ⊢ (𝜑 → ¬ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵))

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 class class class wbr 5106 ran crn 5656 ‘cfv 6558 (class class class)co 7443 Basecbs 17416 distcds 17466 TarskiGcstrkg 28919 Itvcitv 28925 LineGclng 28926 hlGchlg 29093 pInvGcmir 29154 midGcmid 29307

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

This theorem is used by: tgextancgra 33104

W3C validator