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 29318

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 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
7		eqid 2760	. . . . . 6 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
8		prlngmid2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
9		prlngmid2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
10		prlngmid2.3	. . . . . 6 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11	1, 7, 2, 5, 8, 9, 10	tgelrnln 28977	. . . . 5 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
12		prlngmid2.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
13	1, 2, 3, 5, 11, 12	tgelrnpln 29133	. . . 4 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
14	13	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
15	1, 7, 2, 3, 5, 11, 12	elplnglnid 29140	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
16	15	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
17	1, 7, 2, 3, 5, 11, 12	elplngid 29139	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
18		prlngmid2.2	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))
19	18	fveq2d 6882	. . . . . . . 8 ⊢ (𝜑 → ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑌𝑀𝑊)))
20	19	fveq1d 6880	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
21		prlngmid2.m	. . . . . . . . . 10 ⊢ 𝑀 = (midG‘𝐺)
22	21	oveqi 7426	. . . . . . . . 9 ⊢ (𝑌𝑀𝑊) = (𝑌(midG‘𝐺)𝑊)
23	22	eqcomi 2769	. . . . . . . 8 ⊢ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)
24		eqid 2760	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
25	12	eldifad 3911	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
26	12	eldifbd 3912	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
27	10	neneqd 2960	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑋 = 𝑌)
28		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (¬ 𝑍 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑋 = 𝑌))
29	26, 27, 28	sylanbrc 595	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
30	1, 2, 7, 5, 8, 9, 25, 29	ncoltgdim2 28907	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31		prlngmid2.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
32		eqid 2760	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
33	21	oveqi 7426	. . . . . . . . . . 11 ⊢ (𝑋𝑀𝑍) = (𝑋(midG‘𝐺)𝑍)
34	1, 24, 7, 5, 30, 8, 25	midcl 29161	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ 𝑃)
35	33, 34	eqeltrid 2864	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ 𝑃)
36	18, 35	eqeltrrd 2861	. . . . . . . . 9 ⊢ (𝜑 → (𝑌𝑀𝑊) ∈ 𝑃)
37	1, 24, 7, 5, 30, 9, 31, 32, 36	ismidb 29162	. . . . . . . 8 ⊢ (𝜑 → (𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌) ↔ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)))
38	23, 37	mpbiri 261	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
39	20, 38	eqtr4d 2798	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
40		eqid 2760	. . . . . . 7 ⊢ ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑋𝑀𝑍))
41	1, 7, 2, 5, 8, 9, 10	tglinerflx1 28980	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (𝑋𝐿𝑌))
42	15, 41	sseldd 3932	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
43		nelne2 3053	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
44	41, 26, 43	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
45	1, 7, 2, 3, 5, 13, 42, 17, 44	lnssplng1 29150	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
46	1, 24, 7, 5, 30, 8, 25	midbtwn 29163	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
47	33, 46	eqeltrid 2864	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
48	1, 7, 2, 5, 8, 25, 35, 44, 47	btwnlng1 28966	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
49	45, 48	sseldd 3932	. . . . . . 7 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
50	1, 7, 2, 5, 8, 9, 10	tglinerflx2 28981	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
51	15, 50	sseldd 3932	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
52	1, 3, 32, 40, 5, 13, 49, 51	mirplncl 29152	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
53	39, 52	eqeltrrd 2861	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
54	5	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝐺 ∈ TarskiG)
55	35	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (𝑋𝑀𝑍) ∈ 𝑃)
56	8	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 ∈ 𝑃)
57	9	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑌 ∈ 𝑃)
58	33	eqcomi 2769	. . . . . . . . . . 11 ⊢ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)
59	1, 24, 7, 5, 30, 8, 25, 32, 35	ismidb 29162	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)))
60	58, 59	mpbiri 261	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋))
61	60	eqcomd 2766	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
62	61	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
63		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑍 = 𝑊)
64	39	eqcomd 2766	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
65	64	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
66	62, 63, 65	3eqtrd 2799	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
67	1, 24, 7, 2, 32, 54, 55, 40, 56, 57, 66	mireq 29016	. . . . . 6 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 = 𝑌)
68	10, 67	mteqand 3046	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
69	1, 7, 2, 3, 5, 13, 17, 53, 68	lnssplng1 29150	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
70	69	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
71	41	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
72	16, 71	sseldd 3932	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
73	17	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
74	44	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
75	1, 7, 2, 3, 6, 14, 72, 73, 74	lnssplng1 29150	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
76	48	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
77	75, 76	sseldd 3932	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
78		simplr 781	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑋𝐿𝑌))
79	16, 78	sseldd 3932	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
80	5	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
81	8	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ∈ 𝑃)
82	35	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
83	25	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
84		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 = (𝑋𝑀𝑍))
85	84, 33	eqtr2di 2812	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑋(midG‘𝐺)𝑍) = 𝑋)
86	1, 24, 7, 5, 30, 8, 25, 32, 8	ismidb 29162	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
87	86	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
88	85, 87	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋))
89		eqid 2760	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
90	1, 24, 7, 2, 32, 5, 8, 89	mircinv 29019	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
91	90	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
92	88, 91	eqtr2d 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 = 𝑍)
93	41	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 ∈ (𝑋𝐿𝑌))
94	92, 93	eqeltrrd 2861	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 ∈ (𝑋𝐿𝑌))
95	26, 94	mtand 828	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 = (𝑋𝑀𝑍))
96	95	neqned 2962	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≠ (𝑋𝑀𝑍))
97	96	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ (𝑋𝑀𝑍))
98	1, 7, 2, 5, 8, 25, 44	tglinecom 28982	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐿𝑍) = (𝑍𝐿𝑋))
99	48, 98	eleqtrd 2862	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
100	99	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
101	44	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
102	101	necomd 3010	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑋)
103	1, 7, 2, 80, 81, 82, 83, 97, 100, 102	lnrot1 28970	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑋𝐿(𝑋𝑀𝑍)))
104	11	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
105	41	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
106		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
107	1, 7, 2, 80, 81, 82, 97, 97, 104, 105, 106	tglinethru 28983	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) = (𝑋𝐿(𝑋𝑀𝑍)))
108	103, 107	eleqtrrd 2863	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑋𝐿𝑌))
109	26, 108	mtand 828	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
110	109	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
111		nelne2 3053	. . . . . 6 ⊢ ((𝑒 ∈ (𝑋𝐿𝑌) ∧ ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
112	78, 110, 111	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
113	112	necomd 3010	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ 𝑒)
114	1, 7, 2, 3, 6, 14, 77, 79, 113	lnssplng1 29150	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
115	11	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
116	1, 2, 7, 6, 115, 78	tglnpt 28891	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ 𝑃)
117	35	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
118	1, 7, 2, 6, 116, 117, 112	tglinecom 28982	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
119	1, 7, 2, 6, 116, 117, 112	tgelrnln 28977	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) ∈ ran 𝐿)
120		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
121	118, 120	eqbrtrd 5127	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍))(⟂G‘𝐺)(𝑋𝐿𝑌))
122	1, 24, 7, 2, 6, 119, 115, 121	perpcom 29067	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
123	118, 122	breq2dd 5122	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
124	6	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
125	1, 7, 2, 5, 25, 31, 68	tgelrnln 28977	. . . . . . 7 ⊢ (𝜑 → (𝑍𝐿𝑊) ∈ ran 𝐿)
126	125	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
127	126	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
128	118, 119	eqeltrrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ∈ ran 𝐿)
129	128	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ((𝑋𝑀𝑍)𝐿𝑒) ∈ ran 𝐿)
130		simpr 490	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
131	8	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ 𝑃)
132	9	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑌 ∈ 𝑃)
133	10	necomd 3010	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
134	133	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑌 ≠ 𝑋)
135	1, 2, 32, 40, 6, 117, 116, 131, 132, 134, 78	mirlni 29046	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)))
136	61, 39	oveq12d 7431	. . . . . . . . . 10 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
137	136	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
138	135, 137	eleqtrd 2862	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ (𝑍𝐿𝑊))
139	1, 7, 2, 6, 117, 116, 113	tglinerflx1 28980	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
140	1, 7, 2, 6, 117, 116, 113	tglinerflx2 28981	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝑀𝑍)𝐿𝑒))
141	1, 24, 7, 2, 32, 6, 40, 128, 139, 140	mirln 29027	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
142	138, 141	elind 4146	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
143	142	adantr 486	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
144	130, 143	eqeltrd 2860	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
145	1, 7, 2, 5, 25, 31, 68	tglinerflx2 28981	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (𝑍𝐿𝑊))
146	145	ad3antrrr 743	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ∈ (𝑍𝐿𝑊))
147	139	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
148	68	necomd 3010	. . . . . 6 ⊢ (𝜑 → 𝑊 ≠ 𝑍)
149	148	ad3antrrr 743	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ≠ 𝑍)
150	1, 24, 7, 2, 32, 6, 117, 40, 116, 112	mirne 29018	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ≠ (𝑋𝑀𝑍))
151	150	necomd 3010	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
152	151	adantr 486	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
153	152, 130	neeqtrrd 3029	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ 𝑍)
154	39	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
155	130	eqcomd 2766	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = 𝑍)
156	1, 24, 7, 2, 32, 5, 35, 40	mircinv 29019	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
157	156	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
158	157	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
159	154, 155, 158	s3eqd 14935	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑊𝑍(𝑋𝑀𝑍)”⟩)
160	132	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑌 ∈ 𝑃)
161	116	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ 𝑃)
162	117	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ 𝑃)
163	131	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑋 ∈ 𝑃)
164	1, 7, 2, 6, 132, 131, 116, 134, 78	lncom 28969	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑌𝐿𝑋))
165	164	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ (𝑌𝐿𝑋))
166	1, 7, 2, 5, 8, 9, 10	tglinecom 28982	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋𝐿𝑌) = (𝑌𝐿𝑋))
167	166	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌) = (𝑌𝐿𝑋))
168	115	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
169		simplr 781	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
170	1, 24, 7, 2, 124, 129, 168, 169	perpcom 29067	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
171	167, 170	eqbrtrrd 5129	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
172	118	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
173	171, 172	breqtrrd 5133	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
174	1, 24, 7, 2, 124, 160, 163, 165, 162, 173	perprag 29081	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑌𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
175	1, 24, 7, 2, 32, 124, 160, 161, 162, 174, 40, 162	mirrag 29055	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
176	159, 175	eqeltrrd 2861	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑊𝑍(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
177	1, 24, 7, 2, 124, 127, 129, 144, 146, 147, 149, 153, 176	ragperp 29071	. . . 4 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
178	6	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
179	126	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
180	128	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ((𝑋𝑀𝑍)𝐿𝑒) ∈ ran 𝐿)
181	142	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
182	1, 7, 2, 5, 25, 31, 68	tglinerflx1 28980	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ (𝑍𝐿𝑊))
183	182	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑍 ∈ (𝑍𝐿𝑊))
184	183	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ∈ (𝑍𝐿𝑊))
185	139	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
186		simpr 490	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
187	151	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
188	61	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
189		eqidd 2761	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
190	188, 189, 157	s3eqd 14935	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩)
191	1, 24, 7, 2, 6, 131, 132, 78, 117, 122	perprag 29081	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑋𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
192	1, 24, 7, 2, 32, 6, 131, 116, 117, 191, 40, 117	mirrag 29055	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
193	190, 192	eqeltrrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
194	193	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
195	1, 24, 7, 2, 178, 179, 180, 181, 184, 185, 186, 187, 194	ragperp 29071	. . . 4 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
196	177, 195	pm2.61dane 3042	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
197	1, 2, 3, 4, 6, 14, 16, 70, 114, 123, 196	perpprlng 29307	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))
198	1, 24, 7, 2, 5, 11, 35, 109	footex 29075	. 2 ⊢ (𝜑 → ∃𝑒 ∈ (𝑋𝐿𝑌)((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
199	197, 198	r19.29a 3170	1 ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∖ cdif 3896 ∩ cin 3898 ⊆ wss 3899 class class class wbr 5103 ran crn 5656 ‘cfv 6533 (class class class)co 7413 ⟨“cs3 14913 Basecbs 17301 distcds 17351 TarskiGcstrkg 28768 TarskiG_Ecstrkge 28773 Itvcitv 28774 LineGclng 28775 pInvGcmir 29003 ∟Gcrag 29047 ⟂Gcperpg 29049 hlGcplng 29130 midGcmid 29156 parlnGcprlng 29293

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-cnex 11180 ax-resscn 11181 ax-1cn 11182 ax-icn 11183 ax-addcl 11184 ax-addrcl 11185 ax-mulcl 11186 ax-mulrcl 11187 ax-mulcom 11188 ax-addass 11189 ax-mulass 11190 ax-distr 11191 ax-i2m1 11192 ax-1ne0 11193 ax-1rid 11194 ax-rnegex 11195 ax-rrecex 11196 ax-cnre 11197 ax-pre-lttri 11198 ax-pre-lttrn 11199 ax-pre-ltadd 11200 ax-pre-mulgt0 11201

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 2100 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 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 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 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-oadd 8459 df-er 8696 df-map 8828 df-pm 8829 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-dju 9906 df-card 9944 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11467 df-neg 11468 df-nn 12258 df-2 12327 df-3 12328 df-n0 12529 df-xnn0 12602 df-z 12616 df-uz 12888 df-fz 13562 df-fzo 13710 df-hash 14395 df-word 14579 df-concat 14636 df-s1 14663 df-s2 14919 df-s3 14920 df-trkgc 28789 df-trkgb 28790 df-trkgcb 28791 df-trkgld 28793 df-trkg 28794 df-cgrg 28853 df-ismt 28875 df-leg 28925 df-hlg 28943 df-mir 29004 df-rag 29048 df-perpg 29050 df-hpg 29115 df-plng 29131 df-mid 29158 df-lmi 29159 df-cgra 29194 df-prlng 29294

This theorem is used by: symquadprlng 29319 prlngsymquadlem 29320

W3C validator