prlngmid2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prlngmid2		Structured version Visualization version GIF version

Theorem prlngmid2 29222

Description: If the midpoints of two segments (𝑋𝐼𝑍) and (𝑌𝐼𝑊) coincide, the points 𝑋, 𝑌, 𝑍 and 𝑊 form a parallelogram, i.e. the lines (𝑋𝐿𝑌) and (𝑍𝐿𝑊) are parallel. Theorem 12.17 of [Schwabhauser] p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026.)

**Hypotheses**
Ref	Expression
prlngmid2.b	⊢ 𝑃 = (Base‘𝐺)
prlngmid2.l	⊢ 𝐿 = (LineG‘𝐺)
prlngmid2.e	⊢ 𝐸 = (hlG‘𝐺)
prlngmid2.p	⊢ ∥ = (parlnG‘𝐺)
prlngmid2.m	⊢ 𝑀 = (midG‘𝐺)
prlngmid2.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
prlngmid2.1	⊢ (𝜑 → 𝐺 ∈ TarskiG_E)
prlngmid2.x	⊢ (𝜑 → 𝑋 ∈ 𝑃)
prlngmid2.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
prlngmid2.z	⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
prlngmid2.w	⊢ (𝜑 → 𝑊 ∈ 𝑃)
prlngmid2.2	⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))
prlngmid2.3	⊢ (𝜑 → 𝑋 ≠ 𝑌)

**Assertion**
Ref	Expression
prlngmid2	⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))

Proof of Theorem prlngmid2 Dummy variable 𝑒 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		prlngmid2.b	. . 3 ⊢ 𝑃 = (Base‘𝐺)
2		prlngmid2.l	. . 3 ⊢ 𝐿 = (LineG‘𝐺)
3		prlngmid2.e	. . 3 ⊢ 𝐸 = (hlG‘𝐺)
4		prlngmid2.p	. . 3 ⊢ ∥ = (parlnG‘𝐺)
5		prlngmid2.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6	5	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
7		eqid 2762	. . . . . 6 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
8		prlngmid2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
9		prlngmid2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
10		prlngmid2.3	. . . . . 6 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11	1, 7, 2, 5, 8, 9, 10	tgelrnln 28914	. . . . 5 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
12		prlngmid2.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
13	1, 2, 3, 5, 11, 12	tgelrnpln 29069	. . . 4 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
14	13	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
15	1, 7, 2, 3, 5, 11, 12	elplnglnid 29076	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
16	15	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
17	1, 7, 2, 3, 5, 11, 12	elplngid 29075	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
18		prlngmid2.2	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))
19	18	fveq2d 6885	. . . . . . . 8 ⊢ (𝜑 → ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑌𝑀𝑊)))
20	19	fveq1d 6883	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
21		prlngmid2.m	. . . . . . . . . 10 ⊢ 𝑀 = (midG‘𝐺)
22	21	oveqi 7425	. . . . . . . . 9 ⊢ (𝑌𝑀𝑊) = (𝑌(midG‘𝐺)𝑊)
23	22	eqcomi 2771	. . . . . . . 8 ⊢ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)
24		eqid 2762	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
25	12	eldifad 3916	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
26	12	eldifbd 3917	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
27	10	neneqd 2962	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑋 = 𝑌)
28		ioran 998	. . . . . . . . . . 11 ⊢ (¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (¬ 𝑍 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑋 = 𝑌))
29	26, 27, 28	sylanbrc 594	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
30	1, 2, 7, 5, 8, 9, 25, 29	ncoltgdim2 28845	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31		prlngmid2.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
32		eqid 2762	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
33	21	oveqi 7425	. . . . . . . . . . 11 ⊢ (𝑋𝑀𝑍) = (𝑋(midG‘𝐺)𝑍)
34	1, 24, 7, 5, 30, 8, 25	midcl 29097	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ 𝑃)
35	33, 34	eqeltrid 2866	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ 𝑃)
36	18, 35	eqeltrrd 2863	. . . . . . . . 9 ⊢ (𝜑 → (𝑌𝑀𝑊) ∈ 𝑃)
37	1, 24, 7, 5, 30, 9, 31, 32, 36	ismidb 29098	. . . . . . . 8 ⊢ (𝜑 → (𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌) ↔ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)))
38	23, 37	mpbiri 261	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
39	20, 38	eqtr4d 2800	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
40		eqid 2762	. . . . . . 7 ⊢ ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑋𝑀𝑍))
41	1, 7, 2, 5, 8, 9, 10	tglinerflx1 28917	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (𝑋𝐿𝑌))
42	15, 41	sseldd 3937	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
43		nelne2 3055	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
44	41, 26, 43	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
45	1, 7, 2, 3, 5, 13, 42, 17, 44	lnssplng1 29086	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
46	1, 24, 7, 5, 30, 8, 25	midbtwn 29099	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
47	33, 46	eqeltrid 2866	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
48	1, 7, 2, 5, 8, 25, 35, 44, 47	btwnlng1 28903	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
49	45, 48	sseldd 3937	. . . . . . 7 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
50	1, 7, 2, 5, 8, 9, 10	tglinerflx2 28918	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
51	15, 50	sseldd 3937	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
52	1, 3, 32, 40, 5, 13, 49, 51	mirplncl 29088	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
53	39, 52	eqeltrrd 2863	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
54	5	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝐺 ∈ TarskiG)
55	35	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (𝑋𝑀𝑍) ∈ 𝑃)
56	8	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 ∈ 𝑃)
57	9	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑌 ∈ 𝑃)
58	33	eqcomi 2771	. . . . . . . . . . 11 ⊢ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)
59	1, 24, 7, 5, 30, 8, 25, 32, 35	ismidb 29098	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)))
60	58, 59	mpbiri 261	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋))
61	60	eqcomd 2768	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
62	61	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
63		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑍 = 𝑊)
64	39	eqcomd 2768	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
65	64	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
66	62, 63, 65	3eqtrd 2801	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
67	1, 24, 7, 2, 32, 54, 55, 40, 56, 57, 66	mireq 28953	. . . . . 6 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 = 𝑌)
68	10, 67	mteqand 3048	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
69	1, 7, 2, 3, 5, 13, 17, 53, 68	lnssplng1 29086	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
70	69	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
71	41	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
72	16, 71	sseldd 3937	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
73	17	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
74	44	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
75	1, 7, 2, 3, 6, 14, 72, 73, 74	lnssplng1 29086	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
76	48	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
77	75, 76	sseldd 3937	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
78		simplr 780	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑋𝐿𝑌))
79	16, 78	sseldd 3937	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
80	5	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
81	8	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ∈ 𝑃)
82	35	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
83	25	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
84		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 = (𝑋𝑀𝑍))
85	84, 33	eqtr2di 2814	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑋(midG‘𝐺)𝑍) = 𝑋)
86	1, 24, 7, 5, 30, 8, 25, 32, 8	ismidb 29098	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
87	86	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
88	85, 87	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋))
89		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
90	1, 24, 7, 2, 32, 5, 8, 89	mircinv 28956	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
91	90	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
92	88, 91	eqtr2d 2798	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 = 𝑍)
93	41	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 ∈ (𝑋𝐿𝑌))
94	92, 93	eqeltrrd 2863	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 ∈ (𝑋𝐿𝑌))
95	26, 94	mtand 827	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 = (𝑋𝑀𝑍))
96	95	neqned 2964	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≠ (𝑋𝑀𝑍))
97	96	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ (𝑋𝑀𝑍))
98	1, 7, 2, 5, 8, 25, 44	tglinecom 28919	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐿𝑍) = (𝑍𝐿𝑋))
99	48, 98	eleqtrd 2864	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
100	99	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
101	44	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
102	101	necomd 3012	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑋)
103	1, 7, 2, 80, 81, 82, 83, 97, 100, 102	lnrot1 28907	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑋𝐿(𝑋𝑀𝑍)))
104	11	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
105	41	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
106		simpr 489	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
107	1, 7, 2, 80, 81, 82, 97, 97, 104, 105, 106	tglinethru 28920	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) = (𝑋𝐿(𝑋𝑀𝑍)))
108	103, 107	eleqtrrd 2865	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑋𝐿𝑌))
109	26, 108	mtand 827	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
110	109	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
111		nelne2 3055	. . . . . 6 ⊢ ((𝑒 ∈ (𝑋𝐿𝑌) ∧ ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
112	78, 110, 111	syl2anc 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
113	112	necomd 3012	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ 𝑒)
114	1, 7, 2, 3, 6, 14, 77, 79, 113	lnssplng1 29086	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
115	11	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
116	1, 2, 7, 6, 115, 78	tglnpt 28829	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ 𝑃)
117	35	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
118	1, 7, 2, 6, 116, 117, 112	tglinecom 28919	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
119	1, 7, 2, 6, 116, 117, 112	tgelrnln 28914	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) ∈ ran 𝐿)
120		simpr 489	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
121	118, 120	eqbrtrd 5132	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍))(⟂G‘𝐺)(𝑋𝐿𝑌))
122	1, 24, 7, 2, 6, 119, 115, 121	perpcom 29004	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
123	118, 122	breq2dd 5127	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
124	6	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
125	1, 7, 2, 5, 25, 31, 68	tgelrnln 28914	. . . . . . 7 ⊢ (𝜑 → (𝑍𝐿𝑊) ∈ ran 𝐿)
126	125	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
127	126	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
128	118, 119	eqeltrrd 2863	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ∈ ran 𝐿)
129	128	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ((𝑋𝑀𝑍)𝐿𝑒) ∈ ran 𝐿)
130		simpr 489	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
131	8	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ 𝑃)
132	9	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑌 ∈ 𝑃)
133	10	necomd 3012	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
134	133	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑌 ≠ 𝑋)
135	1, 2, 32, 40, 6, 117, 116, 131, 132, 134, 78	mirlni 28983	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)))
136	61, 39	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
137	136	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
138	135, 137	eleqtrd 2864	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ (𝑍𝐿𝑊))
139	1, 7, 2, 6, 117, 116, 113	tglinerflx1 28917	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
140	1, 7, 2, 6, 117, 116, 113	tglinerflx2 28918	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝑀𝑍)𝐿𝑒))
141	1, 24, 7, 2, 32, 6, 40, 128, 139, 140	mirln 28964	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
142	138, 141	elind 4152	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
143	142	adantr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
144	130, 143	eqeltrd 2862	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
145	1, 7, 2, 5, 25, 31, 68	tglinerflx2 28918	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (𝑍𝐿𝑊))
146	145	ad3antrrr 742	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ∈ (𝑍𝐿𝑊))
147	139	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
148	68	necomd 3012	. . . . . 6 ⊢ (𝜑 → 𝑊 ≠ 𝑍)
149	148	ad3antrrr 742	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ≠ 𝑍)
150	1, 24, 7, 2, 32, 6, 117, 40, 116, 112	mirne 28955	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ≠ (𝑋𝑀𝑍))
151	150	necomd 3012	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
152	151	adantr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
153	152, 130	neeqtrrd 3031	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ 𝑍)
154	39	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
155	130	eqcomd 2768	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = 𝑍)
156	1, 24, 7, 2, 32, 5, 35, 40	mircinv 28956	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
157	156	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
158	157	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
159	154, 155, 158	s3eqd 14908	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑊𝑍(𝑋𝑀𝑍)”⟩)
160	132	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑌 ∈ 𝑃)
161	116	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ 𝑃)
162	117	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ 𝑃)
163	131	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑋 ∈ 𝑃)
164	1, 7, 2, 6, 132, 131, 116, 134, 78	lncom 28906	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑌𝐿𝑋))
165	164	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ (𝑌𝐿𝑋))
166	1, 7, 2, 5, 8, 9, 10	tglinecom 28919	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋𝐿𝑌) = (𝑌𝐿𝑋))
167	166	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌) = (𝑌𝐿𝑋))
168	115	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
169		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
170	1, 24, 7, 2, 124, 129, 168, 169	perpcom 29004	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
171	167, 170	eqbrtrrd 5134	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
172	118	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
173	171, 172	breqtrrd 5138	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
174	1, 24, 7, 2, 124, 160, 163, 165, 162, 173	perprag 29018	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑌𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
175	1, 24, 7, 2, 32, 124, 160, 161, 162, 174, 40, 162	mirrag 28992	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
176	159, 175	eqeltrrd 2863	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑊𝑍(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
177	1, 24, 7, 2, 124, 127, 129, 144, 146, 147, 149, 153, 176	ragperp 29008	. . . 4 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
178	6	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
179	126	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
180	128	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ((𝑋𝑀𝑍)𝐿𝑒) ∈ ran 𝐿)
181	142	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
182	1, 7, 2, 5, 25, 31, 68	tglinerflx1 28917	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ (𝑍𝐿𝑊))
183	182	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑍 ∈ (𝑍𝐿𝑊))
184	183	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ∈ (𝑍𝐿𝑊))
185	139	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
186		simpr 489	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
187	151	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
188	61	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
189		eqidd 2763	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
190	188, 189, 157	s3eqd 14908	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩)
191	1, 24, 7, 2, 6, 131, 132, 78, 117, 122	perprag 29018	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑋𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
192	1, 24, 7, 2, 32, 6, 131, 116, 117, 191, 40, 117	mirrag 28992	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
193	190, 192	eqeltrrd 2863	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
194	193	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
195	1, 24, 7, 2, 178, 179, 180, 181, 184, 185, 186, 187, 194	ragperp 29008	. . . 4 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
196	177, 195	pm2.61dane 3044	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
197	1, 2, 3, 4, 6, 14, 16, 70, 114, 123, 196	perpprlng 29211	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))
198	1, 24, 7, 2, 5, 11, 35, 109	footex 29012	. 2 ⊢ (𝜑 → ∃𝑒 ∈ (𝑋𝐿𝑌)((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
199	197, 198	r19.29a 3172	1 ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∖ cdif 3901 ∩ cin 3903 ⊆ wss 3904 class class class wbr 5108 ran crn 5661 ‘cfv 6536 (class class class)co 7412 ⟨“cs3 14886 Basecbs 17275 distcds 17325 TarskiGcstrkg 28707 TarskiG_Ecstrkge 28712 Itvcitv 28713 LineGclng 28714 pInvGcmir 28940 ∟Gcrag 28984 ⟂Gcperpg 28986 hlGcplng 29066 midGcmid 29092 parlnGcprlng 29197

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-oadd 8455 df-er 8692 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-dju 9894 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-nn 12240 df-2 12309 df-3 12310 df-n0 12511 df-xnn0 12584 df-z 12598 df-uz 12869 df-fz 13542 df-fzo 13690 df-hash 14374 df-word 14558 df-concat 14615 df-s1 14641 df-s2 14892 df-s3 14893 df-trkgc 28728 df-trkgb 28729 df-trkgcb 28730 df-trkgld 28732 df-trkg 28733 df-cgrg 28791 df-ismt 28813 df-leg 28863 df-hlg 28881 df-mir 28941 df-rag 28985 df-perpg 28987 df-hpg 29051 df-plng 29067 df-mid 29094 df-lmi 29095 df-cgra 29130 df-prlng 29198

This theorem is used by: symquadprlng 29223 prlngsymquadlem 29224

W3C validator