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 29466

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 2763	. . . . . 6 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
8		prlngmid2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
9		prlngmid2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
10		prlngmid2.3	. . . . . 6 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11	1, 7, 2, 5, 8, 9, 10	tgelrnln 29125	. . . . 5 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
12		prlngmid2.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
13	1, 2, 3, 5, 11, 12	tgelrnpln 29281	. . . 4 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
14	13	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
15	1, 7, 2, 3, 5, 11, 12	elplnglnid 29288	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
16	15	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
17	1, 7, 2, 3, 5, 11, 12	elplngid 29287	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
18		prlngmid2.2	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))
19	18	fveq2d 6909	. . . . . . . 8 ⊢ (𝜑 → ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑌𝑀𝑊)))
20	19	fveq1d 6907	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
21		prlngmid2.m	. . . . . . . . . 10 ⊢ 𝑀 = (midG‘𝐺)
22	21	oveqi 7453	. . . . . . . . 9 ⊢ (𝑌𝑀𝑊) = (𝑌(midG‘𝐺)𝑊)
23	22	eqcomi 2772	. . . . . . . 8 ⊢ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)
24		eqid 2763	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
25	12	eldifad 4054	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
26	12	eldifbd 4055	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
27	10	neneqd 2964	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑋 = 𝑌)
28		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (¬ 𝑍 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑋 = 𝑌))
29	26, 27, 28	sylanbrc 595	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
30	1, 2, 7, 5, 8, 9, 25, 29	ncoltgdim2 29055	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31		prlngmid2.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
32		eqid 2763	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
33	21	oveqi 7453	. . . . . . . . . . 11 ⊢ (𝑋𝑀𝑍) = (𝑋(midG‘𝐺)𝑍)
34	1, 24, 7, 5, 30, 8, 25	midcl 29309	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ 𝑃)
35	33, 34	eqeltrid 2868	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ 𝑃)
36	18, 35	eqeltrrd 2865	. . . . . . . . 9 ⊢ (𝜑 → (𝑌𝑀𝑊) ∈ 𝑃)
37	1, 24, 7, 5, 30, 9, 31, 32, 36	ismidb 29310	. . . . . . . 8 ⊢ (𝜑 → (𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌) ↔ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)))
38	23, 37	mpbiri 261	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
39	20, 38	eqtr4d 2801	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
40		eqid 2763	. . . . . . 7 ⊢ ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑋𝑀𝑍))
41	1, 7, 2, 5, 8, 9, 10	tglinerflx1 29128	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (𝑋𝐿𝑌))
42	15, 41	sseldd 3914	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
43		nelne2 3057	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
44	41, 26, 43	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
45	1, 7, 2, 3, 5, 13, 42, 17, 44	lnssplng1 29298	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
46	1, 24, 7, 5, 30, 8, 25	midbtwn 29311	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
47	33, 46	eqeltrid 2868	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
48	1, 7, 2, 5, 8, 25, 35, 44, 47	btwnlng1 29114	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
49	45, 48	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
50	1, 7, 2, 5, 8, 9, 10	tglinerflx2 29129	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
51	15, 50	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
52	1, 3, 32, 40, 5, 13, 49, 51	mirplncl 29300	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
53	39, 52	eqeltrrd 2865	. . . . 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 2772	. . . . . . . . . . 11 ⊢ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)
59	1, 24, 7, 5, 30, 8, 25, 32, 35	ismidb 29310	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)))
60	58, 59	mpbiri 261	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋))
61	60	eqcomd 2769	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
62	61	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
63		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑍 = 𝑊)
64	39	eqcomd 2769	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
65	64	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
66	62, 63, 65	3eqtrd 2802	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
67	1, 24, 7, 2, 32, 54, 55, 40, 56, 57, 66	mireq 29164	. . . . . 6 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 = 𝑌)
68	10, 67	mteqand 3050	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
69	1, 7, 2, 3, 5, 13, 17, 53, 68	lnssplng1 29298	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
70	69	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
71	41	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
72	16, 71	sseldd 3914	. . . . . 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 29298	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
76	48	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
77	75, 76	sseldd 3914	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
78		simplr 781	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑋𝐿𝑌))
79	16, 78	sseldd 3914	. . . 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 2815	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑋(midG‘𝐺)𝑍) = 𝑋)
86	1, 24, 7, 5, 30, 8, 25, 32, 8	ismidb 29310	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
87	86	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
88	85, 87	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋))
89		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
90	1, 24, 7, 2, 32, 5, 8, 89	mircinv 29167	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
91	90	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
92	88, 91	eqtr2d 2799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 = 𝑍)
93	41	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 ∈ (𝑋𝐿𝑌))
94	92, 93	eqeltrrd 2865	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 ∈ (𝑋𝐿𝑌))
95	26, 94	mtand 828	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 = (𝑋𝑀𝑍))
96	95	neqned 2966	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≠ (𝑋𝑀𝑍))
97	96	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ (𝑋𝑀𝑍))
98	1, 7, 2, 5, 8, 25, 44	tglinecom 29130	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐿𝑍) = (𝑍𝐿𝑋))
99	48, 98	eleqtrd 2866	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
100	99	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
101	44	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
102	101	necomd 3014	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑋)
103	1, 7, 2, 80, 81, 82, 83, 97, 100, 102	lnrot1 29118	. . . . . . . . 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 29131	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) = (𝑋𝐿(𝑋𝑀𝑍)))
108	103, 107	eleqtrrd 2867	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑋𝐿𝑌))
109	26, 108	mtand 828	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
110	109	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
111		nelne2 3057	. . . . . 6 ⊢ ((𝑒 ∈ (𝑋𝐿𝑌) ∧ ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
112	78, 110, 111	syl2anc 596	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
113	112	necomd 3014	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ 𝑒)
114	1, 7, 2, 3, 6, 14, 77, 79, 113	lnssplng1 29298	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
115	11	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
116	1, 2, 7, 6, 115, 78	tglnpt 29039	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ 𝑃)
117	35	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
118	1, 7, 2, 6, 116, 117, 112	tglinecom 29130	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
119	1, 7, 2, 6, 116, 117, 112	tgelrnln 29125	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) ∈ ran 𝐿)
120		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
121	118, 120	eqbrtrd 5130	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍))(⟂G‘𝐺)(𝑋𝐿𝑌))
122	1, 24, 7, 2, 6, 119, 115, 121	perpcom 29215	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
123	118, 122	breq2dd 5125	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
124	6	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
125	1, 7, 2, 5, 25, 31, 68	tgelrnln 29125	. . . . . . 7 ⊢ (𝜑 → (𝑍𝐿𝑊) ∈ ran 𝐿)
126	125	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
127	126	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
128	118, 119	eqeltrrd 2865	. . . . . 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 3014	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
134	133	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑌 ≠ 𝑋)
135	1, 2, 32, 40, 6, 117, 116, 131, 132, 134, 78	mirlni 29194	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)))
136	61, 39	oveq12d 7458	. . . . . . . . . 10 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
137	136	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
138	135, 137	eleqtrd 2866	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ (𝑍𝐿𝑊))
139	1, 7, 2, 6, 117, 116, 113	tglinerflx1 29128	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
140	1, 7, 2, 6, 117, 116, 113	tglinerflx2 29129	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝑀𝑍)𝐿𝑒))
141	1, 24, 7, 2, 32, 6, 40, 128, 139, 140	mirln 29175	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
142	138, 141	elind 4100	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
143	142	adantr 486	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
144	130, 143	eqeltrd 2864	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
145	1, 7, 2, 5, 25, 31, 68	tglinerflx2 29129	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (𝑍𝐿𝑊))
146	145	ad3antrrr 743	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ∈ (𝑍𝐿𝑊))
147	139	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
148	68	necomd 3014	. . . . . 6 ⊢ (𝜑 → 𝑊 ≠ 𝑍)
149	148	ad3antrrr 743	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ≠ 𝑍)
150	1, 24, 7, 2, 32, 6, 117, 40, 116, 112	mirne 29166	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ≠ (𝑋𝑀𝑍))
151	150	necomd 3014	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
152	151	adantr 486	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
153	152, 130	neeqtrrd 3033	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ 𝑍)
154	39	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
155	130	eqcomd 2769	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = 𝑍)
156	1, 24, 7, 2, 32, 5, 35, 40	mircinv 29167	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
157	156	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
158	157	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
159	154, 155, 158	s3eqd 15040	. . . . . 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 29117	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑌𝐿𝑋))
165	164	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ (𝑌𝐿𝑋))
166	1, 7, 2, 5, 8, 9, 10	tglinecom 29130	. . . . . . . . . . 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 29215	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
171	167, 170	eqbrtrrd 5132	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
172	118	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
173	171, 172	breqtrrd 5136	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
174	1, 24, 7, 2, 124, 160, 163, 165, 162, 173	perprag 29229	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑌𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
175	1, 24, 7, 2, 32, 124, 160, 161, 162, 174, 40, 162	mirrag 29203	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
176	159, 175	eqeltrrd 2865	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑊𝑍(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
177	1, 24, 7, 2, 124, 127, 129, 144, 146, 147, 149, 153, 176	ragperp 29219	. . . 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 29128	. . . . . . 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 2764	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
190	188, 189, 157	s3eqd 15040	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩)
191	1, 24, 7, 2, 6, 131, 132, 78, 117, 122	perprag 29229	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑋𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
192	1, 24, 7, 2, 32, 6, 131, 116, 117, 191, 40, 117	mirrag 29203	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
193	190, 192	eqeltrrd 2865	. . . . . 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 29219	. . . 4 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
196	177, 195	pm2.61dane 3046	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
197	1, 2, 3, 4, 6, 14, 16, 70, 114, 123, 196	perpprlng 29455	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))
198	1, 24, 7, 2, 5, 11, 35, 109	footex 29223	. 2 ⊢ (𝜑 → ∃𝑒 ∈ (𝑋𝐿𝑌)((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
199	197, 198	r19.29a 3174	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 2147 ≠ wne 2959 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 class class class wbr 5106 ran crn 5656 ‘cfv 6555 (class class class)co 7440 ⟨“cs3 15018 Basecbs 17413 distcds 17463 TarskiGcstrkg 28916 TarskiG_Ecstrkge 28921 Itvcitv 28922 LineGclng 28923 pInvGcmir 29151 ∟Gcrag 29195 ⟂Gcperpg 29197 hlGcplng 29278 midGcmid 29304 parlnGcprlng 29441

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 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301

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 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-oadd 8505 df-er 8742 df-map 8874 df-pm 8875 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-dju 10006 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-nn 12360 df-2 12429 df-3 12430 df-n0 12631 df-xnn0 12704 df-z 12718 df-uz 12990 df-fz 13664 df-fzo 13813 df-hash 14499 df-word 14683 df-concat 14740 df-s1 14767 df-s2 15024 df-s3 15025 df-trkgc 28937 df-trkgb 28938 df-trkgcb 28939 df-trkgld 28941 df-trkg 28942 df-cgrg 29001 df-ismt 29023 df-leg 29073 df-hlg 29091 df-mir 29152 df-rag 29196 df-perpg 29198 df-hpg 29263 df-plng 29279 df-mid 29306 df-lmi 29307 df-cgra 29342 df-prlng 29442

This theorem is used by: symquadprlng 29467 prlngsymquadlem 29468

W3C validator