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 33072

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 29149, the converse of the mirln 29148 used in tgextamirn 33067, 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 29283 / mirinv 29138 / mirne 29139, not from midbtwn 29284. (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 29024	. . . 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 29028	. . . . . . 7 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
17	1, 15, 3, 4, 16, 7, 6	midcl 29282	. . . . . 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 29028	. . . . . . . 8 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
21	1, 15, 3, 4, 20, 7, 6	midcl 29282	. . . . . . 7 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
22	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . 8 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
23	1, 15, 3, 4, 22, 7, 6	midbtwn 29284	. . . . . . 7 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ (𝐴𝐼𝐶))
24	1, 15, 3, 4, 7, 21, 6, 23	tgbtwncom 28951	. . . . . 6 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ (𝐶𝐼𝐴))
25	24	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ (𝐶𝐼𝐴))
26	1, 2, 3, 13, 14, 18, 19, 25	btwncolg3 29020	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴 ∈ (𝐶𝐿(𝐴(midG‘𝐺)𝐶)) ∨ 𝐶 = (𝐴(midG‘𝐺)𝐶)))
27		eqidd 2761	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
28	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
29		eqid 2760	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
30	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31	1, 15, 3, 4, 30, 7, 6	midcl 29282	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
32	1, 15, 3, 4, 28, 7, 6, 29, 31	ismidb 29283	. . . . . . . 8 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
33	27, 32	mpbird 260	. . . . . . 7 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
34		eqid 2760	. . . . . . . 8 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
35	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
36	1, 15, 3, 4, 35, 7, 6	midcl 29282	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
37		eqid 2760	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
38	1, 3, 2, 4, 7, 5, 6, 8	ncolne2 29094	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
39	38	necomd 3010	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐴)
40		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
41	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
42		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
43	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
44	1, 15, 3, 4, 43, 7, 6	midcl 29282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
45	1, 15, 3, 4, 41, 7, 6, 42, 44	ismidb 29283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
46	40, 45	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
47	46	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴))
48		eqid 2760	. . . . . . . . . . . . 13 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
49	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
50	1, 15, 3, 4, 49, 7, 6	midcl 29282	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
51		eqid 2760	. . . . . . . . . . . . 13 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
52	1, 15, 3, 2, 48, 4, 50, 51, 7	mirinv 29138	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
53	47, 52	bitrd 282	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
54	53	necon3bid 2999	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) ≠ 𝐴))
55	39, 54	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐴)
56	55	necomd 3010	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ (𝐴(midG‘𝐺)𝐶))
57	1, 15, 3, 2, 34, 4, 36, 37, 7, 56	mirne 29139	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ≠ (𝐴(midG‘𝐺)𝐶))
58	33, 57	eqnetrd 3022	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ (𝐴(midG‘𝐺)𝐶))
59	58	neneqd 2960	. . . . 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 29024	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
66		ioran 999	. . . . . . . 8 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
67	65, 66	sylib 221	. . . . . . 7 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
68	67	simprd 501	. . . . . 6 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
69	68	neqned 2962	. . . . 5 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
70	69	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐶 ≠ 𝐵)
71	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . 6 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
72	1, 15, 3, 4, 71, 7, 6	midcl 29282	. . . . 5 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
73	72	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
74		eqidd 2761	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
75	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
76		eqid 2760	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
77	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
78	1, 15, 3, 4, 77, 7, 6	midcl 29282	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
79	1, 15, 3, 4, 75, 7, 6, 76, 78	ismidb 29283	. . . . . . . 8 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
80	74, 79	mpbird 260	. . . . . . 7 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
81		eqid 2760	. . . . . . . 8 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
82	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
83	1, 15, 3, 4, 82, 7, 6	midcl 29282	. . . . . . . 8 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
84		eqid 2760	. . . . . . . 8 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
85	1, 3, 2, 4, 7, 5, 6, 8	ncolne2 29094	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
86	85	necomd 3010	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐴)
87		eqidd 2761	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶))
88	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
89		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
90	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
91	1, 15, 3, 4, 90, 7, 6	midcl 29282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
92	1, 15, 3, 4, 88, 7, 6, 89, 91	ismidb 29283	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ↔ (𝐴(midG‘𝐺)𝐶) = (𝐴(midG‘𝐺)𝐶)))
93	87, 92	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴))
94	93	eqeq1d 2762	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴))
95		eqid 2760	. . . . . . . . . . . . 13 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
96	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
97	1, 15, 3, 4, 96, 7, 6	midcl 29282	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
98		eqid 2760	. . . . . . . . . . . . 13 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
99	1, 15, 3, 2, 95, 4, 97, 98, 7	mirinv 29138	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
100	94, 99	bitrd 282	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 = 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) = 𝐴))
101	100	necon3bid 2999	. . . . . . . . . 10 ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ (𝐴(midG‘𝐺)𝐶) ≠ 𝐴))
102	86, 101	mpbid 235	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐴)
103	102	necomd 3010	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ≠ (𝐴(midG‘𝐺)𝐶))
104	1, 15, 3, 2, 81, 4, 83, 84, 7, 103	mirne 29139	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐴) ≠ (𝐴(midG‘𝐺)𝐶))
105	80, 104	eqnetrd 3022	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ (𝐴(midG‘𝐺)𝐶))
106	105	necomd 3010	. . . . 5 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ≠ 𝐶)
107	106	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ≠ 𝐶)
108		eqid 2760	. . . . 5 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
109	4	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐺 ∈ TarskiG)
110		eqid 2760	. . . . 5 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
111	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29024	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
112		ioran 999	. . . . . . . . . 10 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
113	111, 112	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
114	113	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
115	114	neqned 2962	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
116	1, 3, 2, 4, 6, 5, 115	tgelrnln 29098	. . . . . 6 ⊢ (𝜑 → (𝐶𝐿𝐵) ∈ ran 𝐿)
117	116	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐶𝐿𝐵) ∈ ran 𝐿)
118	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . 7 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
119	1, 15, 3, 4, 118, 7, 6	midcl 29282	. . . . . 6 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
120	119	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
121	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29024	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
122		ioran 999	. . . . . . . . . 10 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
123	121, 122	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
124	123	simprd 501	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
125	124	neqned 2962	. . . . . . 7 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
126	1, 3, 2, 4, 6, 5, 125	tglinerflx2 29102	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (𝐶𝐿𝐵))
127	126	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐵 ∈ (𝐶𝐿𝐵))
128		tgextalem1inag.k	. . . . . . . 8 ⊢ 𝐾 = (hlG‘𝐺)
129		eqid 2760	. . . . . . . . . 10 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
130	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
131	1, 15, 3, 4, 130, 7, 6	midcl 29282	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
132		eqid 2760	. . . . . . . . . 10 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
133	1, 15, 3, 2, 129, 4, 131, 132, 5	mircl 29133	. . . . . . . . 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 2760	. . . . . . . . . . 11 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
141	1, 2, 3, 4, 5, 6, 7, 8	ncoltgdim2 29028	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
142	1, 15, 3, 4, 141, 7, 6	midcl 29282	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(midG‘𝐺)𝐶) ∈ 𝑃)
143		eqid 2760	. . . . . . . . . . 11 ⊢ ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶)) = ((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))
144	1, 15, 3, 2, 140, 4, 142, 143, 5	mircl 29133	. . . . . . . . . 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 29070	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)(𝐾‘𝐶)𝐷)
150	1, 3, 128, 134, 136, 137, 138, 2, 149	hlln 29073	. . . . . . 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 3010	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐶)
156	155	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → 𝐷 ≠ 𝐶)
157	1, 3, 2, 151, 152, 153, 156	tglinecom 29103	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐷𝐿𝐶) = (𝐶𝐿𝐷))
158	150, 157	eleqtrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ (𝐶𝐿𝐷))
159	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29024	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
160		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝐴 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵) ↔ (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
161	159, 160	sylib 221	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 𝐴 ∈ (𝐶𝐿𝐵) ∧ ¬ 𝐶 = 𝐵))
162	161	simprd 501	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝐶 = 𝐵)
163	162	neqned 2962	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
164	154	necomd 3010	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ≠ 𝐶)
165		tgextalem1inag.ext	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ (𝐵𝐼𝐷))
166	1, 15, 3, 4, 5, 6, 135, 165	tgbtwncom 28951	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ (𝐷𝐼𝐵))
167	1, 2, 3, 4, 6, 5, 135, 166	btwncolg2 29019	. . . . . . . . 9 ⊢ (𝜑 → (𝐷 ∈ (𝐶𝐿𝐵) ∨ 𝐶 = 𝐵))
168	1, 2, 3, 4, 5, 6, 7, 8	ncolcom 29024	. . . . . . . . . . 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 29100	. . . . . . 7 ⊢ (𝜑 → (𝐶𝐿𝐵) = (𝐶𝐿𝐷))
174	173	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐶𝐿𝐵) = (𝐶𝐿𝐷))
175	158, 174	eleqtrrd 2863	. . . . 5 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵) ∈ (𝐶𝐿𝐵))
176	1, 15, 3, 2, 108, 109, 110, 117, 120, 127, 175	mirln2 29149	. . . 4 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐴(midG‘𝐺)𝐶) ∈ (𝐶𝐿𝐵))
177	1, 3, 2, 62, 63, 64, 70, 73, 107, 176	tglineelsb2 29100	. . 3 ⊢ ((𝜑 ∧ 𝐷(𝐾‘𝐶)(((pInvG‘𝐺)‘(𝐴(midG‘𝐺)𝐶))‘𝐵)) → (𝐶𝐿𝐵) = (𝐶𝐿(𝐴(midG‘𝐺)𝐶)))
178	61, 177	eleqtrrd 2863	. 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 1569 ∈ wcel 2144 ≠ wne 2955 class class class wbr 5102 ran crn 5651 ‘cfv 6538 (class class class)co 7420 Basecbs 17387 distcds 17437 TarskiGcstrkg 28889 Itvcitv 28895 LineGclng 28896 hlGchlg 29063 pInvGcmir 29124 midGcmid 29277

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

This theorem is used by: tgextancgra 33074

W3C validator