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 29187

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 2770	. . . . . 6 ⊢ (Itv‘𝐺) = (Itv‘𝐺)
8		prlngmid2.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
9		prlngmid2.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
10		prlngmid2.3	. . . . . 6 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
11	1, 7, 2, 5, 8, 9, 10	tgelrnln 28883	. . . . 5 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
12		prlngmid2.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
13	1, 2, 3, 5, 11, 12	tgelrnpln 29036	. . . 4 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
14	13	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
15	1, 7, 2, 3, 5, 11, 12	elplnglnid 29043	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
16	15	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
17	1, 7, 2, 3, 5, 11, 12	elplngid 29042	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
18		prlngmid2.2	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))
19	18	fveq2d 6889	. . . . . . . 8 ⊢ (𝜑 → ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑌𝑀𝑊)))
20	19	fveq1d 6887	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
21		prlngmid2.m	. . . . . . . . . 10 ⊢ 𝑀 = (midG‘𝐺)
22	21	oveqi 7427	. . . . . . . . 9 ⊢ (𝑌𝑀𝑊) = (𝑌(midG‘𝐺)𝑊)
23	22	eqcomi 2779	. . . . . . . 8 ⊢ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)
24		eqid 2770	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
25	12	eldifad 3925	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
26	12	eldifbd 3926	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
27	10	neneqd 2970	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 𝑋 = 𝑌)
28		ioran 999	. . . . . . . . . . 11 ⊢ (¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌) ↔ (¬ 𝑍 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑋 = 𝑌))
29	26, 27, 28	sylanbrc 594	. . . . . . . . . 10 ⊢ (𝜑 → ¬ (𝑍 ∈ (𝑋𝐿𝑌) ∨ 𝑋 = 𝑌))
30	1, 2, 7, 5, 8, 9, 25, 29	ncoltgdim2 28814	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31		prlngmid2.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
32		eqid 2770	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
33	21	oveqi 7427	. . . . . . . . . . 11 ⊢ (𝑋𝑀𝑍) = (𝑋(midG‘𝐺)𝑍)
34	1, 24, 7, 5, 30, 8, 25	midcl 29064	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ 𝑃)
35	33, 34	eqeltrid 2874	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ 𝑃)
36	18, 35	eqeltrrd 2871	. . . . . . . . 9 ⊢ (𝜑 → (𝑌𝑀𝑊) ∈ 𝑃)
37	1, 24, 7, 5, 30, 9, 31, 32, 36	ismidb 29065	. . . . . . . 8 ⊢ (𝜑 → (𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌) ↔ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)))
38	23, 37	mpbiri 261	. . . . . . 7 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
39	20, 38	eqtr4d 2808	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
40		eqid 2770	. . . . . . 7 ⊢ ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑋𝑀𝑍))
41	1, 7, 2, 5, 8, 9, 10	tglinerflx1 28886	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (𝑋𝐿𝑌))
42	15, 41	sseldd 3946	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
43		nelne2 3063	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
44	41, 26, 43	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
45	1, 7, 2, 3, 5, 13, 42, 17, 44	lnssplng1 29053	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
46	1, 24, 7, 5, 30, 8, 25	midbtwn 29066	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
47	33, 46	eqeltrid 2874	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
48	1, 7, 2, 5, 8, 25, 35, 44, 47	btwnlng1 28872	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
49	45, 48	sseldd 3946	. . . . . . 7 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
50	1, 7, 2, 5, 8, 9, 10	tglinerflx2 28887	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
51	15, 50	sseldd 3946	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
52	1, 3, 32, 40, 5, 13, 49, 51	mirplncl 29055	. . . . . 6 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
53	39, 52	eqeltrrd 2871	. . . . 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 2779	. . . . . . . . . . 11 ⊢ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)
59	1, 24, 7, 5, 30, 8, 25, 32, 35	ismidb 29065	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = (𝑋𝑀𝑍)))
60	58, 59	mpbiri 261	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋))
61	60	eqcomd 2776	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
62	61	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = 𝑍)
63		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑍 = 𝑊)
64	39	eqcomd 2776	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
65	64	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑊 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
66	62, 63, 65	3eqtrd 2809	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌))
67	1, 24, 7, 2, 32, 54, 55, 40, 56, 57, 66	mireq 28922	. . . . . 6 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 = 𝑌)
68	10, 67	mteqand 3056	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
69	1, 7, 2, 3, 5, 13, 17, 53, 68	lnssplng1 29053	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
70	69	ad2antrr 738	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
71	41	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
72	16, 71	sseldd 3946	. . . . . 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 29053	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
76	48	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
77	75, 76	sseldd 3946	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
78		simplr 780	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑋𝐿𝑌))
79	16, 78	sseldd 3946	. . . 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 2822	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑋(midG‘𝐺)𝑍) = 𝑋)
86	1, 24, 7, 5, 30, 8, 25, 32, 8	ismidb 29065	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
87	86	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋) ↔ (𝑋(midG‘𝐺)𝑍) = 𝑋))
88	85, 87	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 = (((pInvG‘𝐺)‘𝑋)‘𝑋))
89		eqid 2770	. . . . . . . . . . . . . . . . 17 ⊢ ((pInvG‘𝐺)‘𝑋) = ((pInvG‘𝐺)‘𝑋)
90	1, 24, 7, 2, 32, 5, 8, 89	mircinv 28925	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
91	90	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → (((pInvG‘𝐺)‘𝑋)‘𝑋) = 𝑋)
92	88, 91	eqtr2d 2806	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 = 𝑍)
93	41	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑋 ∈ (𝑋𝐿𝑌))
94	92, 93	eqeltrrd 2871	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑋 = (𝑋𝑀𝑍)) → 𝑍 ∈ (𝑋𝐿𝑌))
95	26, 94	mtand 827	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 = (𝑋𝑀𝑍))
96	95	neqned 2972	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≠ (𝑋𝑀𝑍))
97	96	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ (𝑋𝑀𝑍))
98	1, 7, 2, 5, 8, 25, 44	tglinecom 28888	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑋𝐿𝑍) = (𝑍𝐿𝑋))
99	48, 98	eleqtrd 2872	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
100	99	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑍𝐿𝑋))
101	44	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
102	101	necomd 3020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑋)
103	1, 7, 2, 80, 81, 82, 83, 97, 100, 102	lnrot1 28876	. . . . . . . . 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 28889	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) = (𝑋𝐿(𝑋𝑀𝑍)))
108	103, 107	eleqtrrd 2873	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑋𝐿𝑌))
109	26, 108	mtand 827	. . . . . . 7 ⊢ (𝜑 → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
110	109	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌))
111		nelne2 3063	. . . . . 6 ⊢ ((𝑒 ∈ (𝑋𝐿𝑌) ∧ ¬ (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
112	78, 110, 111	syl2anc 595	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ≠ (𝑋𝑀𝑍))
113	112	necomd 3020	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ 𝑒)
114	1, 7, 2, 3, 6, 14, 77, 79, 113	lnssplng1 29053	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
115	11	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
116	1, 2, 7, 6, 115, 78	tglnpt 28798	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ 𝑃)
117	35	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
118	1, 7, 2, 6, 116, 117, 112	tglinecom 28888	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
119	1, 7, 2, 6, 116, 117, 112	tgelrnln 28883	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) ∈ ran 𝐿)
120		simpr 489	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
121	118, 120	eqbrtrd 5138	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍))(⟂G‘𝐺)(𝑋𝐿𝑌))
122	1, 24, 7, 2, 6, 119, 115, 121	perpcom 28972	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
123	118, 122	breq2dd 5133	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
124	6	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
125	1, 7, 2, 5, 25, 31, 68	tgelrnln 28883	. . . . . . 7 ⊢ (𝜑 → (𝑍𝐿𝑊) ∈ ran 𝐿)
126	125	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
127	126	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊) ∈ ran 𝐿)
128	118, 119	eqeltrrd 2871	. . . . . 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 3020	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑋)
134	133	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑌 ≠ 𝑋)
135	1, 2, 32, 40, 6, 117, 116, 131, 132, 134, 78	mirlni 28951	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)))
136	61, 39	oveq12d 7432	. . . . . . . . . 10 ⊢ (𝜑 → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
137	136	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)) = (𝑍𝐿𝑊))
138	135, 137	eleqtrd 2872	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ (𝑍𝐿𝑊))
139	1, 7, 2, 6, 117, 116, 113	tglinerflx1 28886	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
140	1, 7, 2, 6, 117, 116, 113	tglinerflx2 28887	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝑀𝑍)𝐿𝑒))
141	1, 24, 7, 2, 32, 6, 40, 128, 139, 140	mirln 28933	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
142	138, 141	elind 4161	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
143	142	adantr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
144	130, 143	eqeltrd 2870	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑍 ∈ ((𝑍𝐿𝑊) ∩ ((𝑋𝑀𝑍)𝐿𝑒)))
145	1, 7, 2, 5, 25, 31, 68	tglinerflx2 28887	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (𝑍𝐿𝑊))
146	145	ad3antrrr 742	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ∈ (𝑍𝐿𝑊))
147	139	adantr 485	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
148	68	necomd 3020	. . . . . 6 ⊢ (𝜑 → 𝑊 ≠ 𝑍)
149	148	ad3antrrr 742	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑊 ≠ 𝑍)
150	1, 24, 7, 2, 32, 6, 117, 40, 116, 112	mirne 28924	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ≠ (𝑋𝑀𝑍))
151	150	necomd 3020	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
152	151	adantr 485	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
153	152, 130	neeqtrrd 3039	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝑀𝑍) ≠ 𝑍)
154	39	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = 𝑊)
155	130	eqcomd 2776	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = 𝑍)
156	1, 24, 7, 2, 32, 5, 35, 40	mircinv 28925	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
157	156	ad2antrr 738	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
158	157	adantr 485	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
159	154, 155, 158	s3eqd 14904	. . . . . 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 28875	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑌𝐿𝑋))
165	164	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ (𝑌𝐿𝑋))
166	1, 7, 2, 5, 8, 9, 10	tglinecom 28888	. . . . . . . . . . 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 28972	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
171	167, 170	eqbrtrrd 5140	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
172	118	adantr 485	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
173	171, 172	breqtrrd 5144	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
174	1, 24, 7, 2, 124, 160, 163, 165, 162, 173	perprag 28986	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑌𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
175	1, 24, 7, 2, 32, 124, 160, 161, 162, 174, 40, 162	mirrag 28960	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
176	159, 175	eqeltrrd 2871	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑊𝑍(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
177	1, 24, 7, 2, 124, 127, 129, 144, 146, 147, 149, 153, 176	ragperp 28976	. . . 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 28886	. . . . . . 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 2771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒))
190	188, 189, 157	s3eqd 14904	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩)
191	1, 24, 7, 2, 6, 131, 132, 78, 117, 122	perprag 28986	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑋𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
192	1, 24, 7, 2, 32, 6, 131, 116, 117, 191, 40, 117	mirrag 28960	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ ∈ (∟G‘𝐺))
193	190, 192	eqeltrrd 2871	. . . . . 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 28976	. . . 4 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 ≠ (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
196	177, 195	pm2.61dane 3052	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
197	1, 2, 3, 4, 6, 14, 16, 70, 114, 123, 196	perpprlng 29177	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))
198	1, 24, 7, 2, 5, 11, 35, 109	footex 28980	. 2 ⊢ (𝜑 → ∃𝑒 ∈ (𝑋𝐿𝑌)((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
199	197, 198	r19.29a 3180	1 ⊢ (𝜑 → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1568 ∈ wcel 2150 ≠ wne 2965 ∖ cdif 3910 ∩ cin 3912 ⊆ wss 3913 class class class wbr 5114 ran crn 5666 ‘cfv 6540 (class class class)co 7414 ⟨“cs3 14882 Basecbs 17272 distcds 17322 TarskiGcstrkg 28676 TarskiG_Ecstrkge 28681 Itvcitv 28682 LineGclng 28683 pInvGcmir 28909 ∟Gcrag 28952 ⟂Gcperpg 28954 hlGcplng 29033 midGcmid 29059 parlnGcprlng 29163

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2152 ax-9 2160 ax-10 2183 ax-11 2199 ax-12 2220 ax-ext 2742 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5340 ax-pr 5408 ax-un 7736 ax-cnex 11159 ax-resscn 11160 ax-1cn 11161 ax-icn 11162 ax-addcl 11163 ax-addrcl 11164 ax-mulcl 11165 ax-mulrcl 11166 ax-mulcom 11167 ax-addass 11168 ax-mulass 11169 ax-distr 11170 ax-i2m1 11171 ax-1ne0 11172 ax-1rid 11173 ax-rnegex 11174 ax-rrecex 11175 ax-cnre 11176 ax-pre-lttri 11177 ax-pre-lttrn 11178 ax-pre-ltadd 11179 ax-pre-mulgt0 11180

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2099 df-mo 2574 df-eu 2604 df-clab 2749 df-cleq 2762 df-clel 2845 df-nfc 2919 df-ne 2966 df-nel 3072 df-ral 3087 df-rex 3097 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3464 df-sbc 3753 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5560 df-eprel 5565 df-po 5573 df-so 5574 df-fr 5618 df-we 5620 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-oadd 8460 df-er 8697 df-map 8829 df-pm 8830 df-en 8947 df-dom 8948 df-sdom 8949 df-fin 8950 df-dju 9890 df-card 9928 df-pnf 11248 df-mnf 11249 df-xr 11250 df-ltxr 11251 df-le 11252 df-sub 11446 df-neg 11447 df-nn 12237 df-2 12306 df-3 12307 df-n0 12508 df-xnn0 12581 df-z 12595 df-uz 12866 df-fz 13539 df-fzo 13686 df-hash 14370 df-word 14554 df-concat 14611 df-s1 14637 df-s2 14888 df-s3 14889 df-trkgc 28697 df-trkgb 28698 df-trkgcb 28699 df-trkgld 28701 df-trkg 28702 df-cgrg 28760 df-ismt 28782 df-leg 28832 df-hlg 28850 df-mir 28910 df-rag 28953 df-perpg 28955 df-hpg 29019 df-plng 29034 df-mid 29061 df-lmi 29062 df-cgra 29096 df-prlng 29164

This theorem is referenced by: (None)

W3C validator