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 29372

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 29031	. . . . 5 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
12		prlngmid2.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
13	1, 2, 3, 5, 11, 12	tgelrnpln 29187	. . . 4 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
14	13	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝐿𝑌)𝐸𝑍) ∈ ran 𝐸)
15	1, 7, 2, 3, 5, 11, 12	elplnglnid 29194	. . . 4 ⊢ (𝜑 → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
16	15	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
17	1, 7, 2, 3, 5, 11, 12	elplngid 29193	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
18		prlngmid2.2	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) = (𝑌𝑀𝑊))
19	18	fveq2d 6877	. . . . . . . 8 ⊢ (𝜑 → ((pInvG‘𝐺)‘(𝑋𝑀𝑍)) = ((pInvG‘𝐺)‘(𝑌𝑀𝑊)))
20	19	fveq1d 6875	. . . . . . 7 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌) = (((pInvG‘𝐺)‘(𝑌𝑀𝑊))‘𝑌))
21		prlngmid2.m	. . . . . . . . . 10 ⊢ 𝑀 = (midG‘𝐺)
22	21	oveqi 7421	. . . . . . . . 9 ⊢ (𝑌𝑀𝑊) = (𝑌(midG‘𝐺)𝑊)
23	22	eqcomi 2769	. . . . . . . 8 ⊢ (𝑌(midG‘𝐺)𝑊) = (𝑌𝑀𝑊)
24		eqid 2760	. . . . . . . . 9 ⊢ (dist‘𝐺) = (dist‘𝐺)
25	12	eldifad 3910	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
26	12	eldifbd 3911	. . . . . . . . . . 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 28961	. . . . . . . . 9 ⊢ (𝜑 → 𝐺Dim_TarskiG≥2)
31		prlngmid2.w	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
32		eqid 2760	. . . . . . . . 9 ⊢ (pInvG‘𝐺) = (pInvG‘𝐺)
33	21	oveqi 7421	. . . . . . . . . . 11 ⊢ (𝑋𝑀𝑍) = (𝑋(midG‘𝐺)𝑍)
34	1, 24, 7, 5, 30, 8, 25	midcl 29215	. . . . . . . . . . 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 29216	. . . . . . . 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 29034	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ (𝑋𝐿𝑌))
42	15, 41	sseldd 3931	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
43		nelne2 3053	. . . . . . . . . 10 ⊢ ((𝑋 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑍)
44	41, 26, 43	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ≠ 𝑍)
45	1, 7, 2, 3, 5, 13, 42, 17, 44	lnssplng1 29204	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
46	1, 24, 7, 5, 30, 8, 25	midbtwn 29217	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋(midG‘𝐺)𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
47	33, 46	eqeltrid 2864	. . . . . . . . 9 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋(Itv‘𝐺)𝑍))
48	1, 7, 2, 5, 8, 25, 35, 44, 47	btwnlng1 29020	. . . . . . . 8 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
49	45, 48	sseldd 3931	. . . . . . 7 ⊢ (𝜑 → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
50	1, 7, 2, 5, 8, 9, 10	tglinerflx2 29035	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
51	15, 50	sseldd 3931	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
52	1, 3, 32, 40, 5, 13, 49, 51	mirplncl 29206	. . . . . 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 29216	. . . . . . . . . . 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 29070	. . . . . 6 ⊢ ((𝜑 ∧ 𝑍 = 𝑊) → 𝑋 = 𝑌)
68	10, 67	mteqand 3046	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
69	1, 7, 2, 3, 5, 13, 17, 53, 68	lnssplng1 29204	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
70	69	ad2antrr 739	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑍𝐿𝑊) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
71	41	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑋 ∈ (𝑋𝐿𝑌))
72	16, 71	sseldd 3931	. . . . . 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 29204	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑍) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
76	48	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ (𝑋𝐿𝑍))
77	75, 76	sseldd 3931	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝐿𝑌)𝐸𝑍))
78		simplr 781	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑋𝐿𝑌))
79	16, 78	sseldd 3931	. . . 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 29216	. . . . . . . . . . . . . . . . 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 29073	. . . . . . . . . . . . . . . 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 29036	. . . . . . . . . . . 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 29024	. . . . . . . . 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 29037	. . . . . . . . 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 29204	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒) ⊆ ((𝑋𝐿𝑌)𝐸𝑍))
115	11	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
116	1, 2, 7, 6, 115, 78	tglnpt 28945	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ 𝑃)
117	35	ad2antrr 739	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ 𝑃)
118	1, 7, 2, 6, 116, 117, 112	tglinecom 29036	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
119	1, 7, 2, 6, 116, 117, 112	tgelrnln 29031	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍)) ∈ ran 𝐿)
120		simpr 490	. . . . . 6 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌))
121	118, 120	eqbrtrd 5126	. . . . 5 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑒𝐿(𝑋𝑀𝑍))(⟂G‘𝐺)(𝑋𝐿𝑌))
122	1, 24, 7, 2, 6, 119, 115, 121	perpcom 29121	. . . 4 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
123	118, 122	breq2dd 5121	. . 3 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
124	6	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝐺 ∈ TarskiG)
125	1, 7, 2, 5, 25, 31, 68	tgelrnln 29031	. . . . . . 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 29100	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)𝐿(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑌)))
136	61, 39	oveq12d 7426	. . . . . . . . . 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 29034	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝑀𝑍) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
140	1, 7, 2, 6, 117, 116, 113	tglinerflx2 29035	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ ((𝑋𝑀𝑍)𝐿𝑒))
141	1, 24, 7, 2, 32, 6, 40, 128, 139, 140	mirln 29081	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒) ∈ ((𝑋𝑀𝑍)𝐿𝑒))
142	138, 141	elind 4145	. . . . . . 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 29035	. . . . . 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 29072	. . . . . . . 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 29073	. . . . . . . . 9 ⊢ (𝜑 → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
157	156	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
158	157	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍)) = (𝑋𝑀𝑍))
159	154, 155, 158	s3eqd 14982	. . . . . 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 29023	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → 𝑒 ∈ (𝑌𝐿𝑋))
165	164	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → 𝑒 ∈ (𝑌𝐿𝑋))
166	1, 7, 2, 5, 8, 9, 10	tglinecom 29036	. . . . . . . . . . 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 29121	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑋𝐿𝑌)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
171	167, 170	eqbrtrrd 5128	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)((𝑋𝑀𝑍)𝐿𝑒))
172	118	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑒𝐿(𝑋𝑀𝑍)) = ((𝑋𝑀𝑍)𝐿𝑒))
173	171, 172	breqtrrd 5132	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → (𝑌𝐿𝑋)(⟂G‘𝐺)(𝑒𝐿(𝑋𝑀𝑍)))
174	1, 24, 7, 2, 124, 160, 163, 165, 162, 173	perprag 29135	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) ∧ 𝑍 = (((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)) → ⟨“𝑌𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
175	1, 24, 7, 2, 32, 124, 160, 161, 162, 174, 40, 162	mirrag 29109	. . . . . 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 29125	. . . 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 29034	. . . . . . 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 14982	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑋)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘(𝑋𝑀𝑍))”⟩ = ⟨“𝑍(((pInvG‘𝐺)‘(𝑋𝑀𝑍))‘𝑒)(𝑋𝑀𝑍)”⟩)
191	1, 24, 7, 2, 6, 131, 132, 78, 117, 122	perprag 29135	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → ⟨“𝑋𝑒(𝑋𝑀𝑍)”⟩ ∈ (∟G‘𝐺))
192	1, 24, 7, 2, 32, 6, 131, 116, 117, 191, 40, 117	mirrag 29109	. . . . . . 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 29125	. . . 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 29361	. 2 ⊢ (((𝜑 ∧ 𝑒 ∈ (𝑋𝐿𝑌)) ∧ ((𝑋𝑀𝑍)𝐿𝑒)(⟂G‘𝐺)(𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∥ (𝑍𝐿𝑊))
198	1, 24, 7, 2, 5, 11, 35, 109	footex 29129	. 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 3895 ∩ cin 3897 ⊆ wss 3898 class class class wbr 5102 ran crn 5648 ‘cfv 6527 (class class class)co 7408 ⟨“cs3 14960 Basecbs 17348 distcds 17398 TarskiGcstrkg 28822 TarskiG_Ecstrkge 28827 Itvcitv 28828 LineGclng 28829 pInvGcmir 29057 ∟Gcrag 29101 ⟂Gcperpg 29103 hlGcplng 29184 midGcmid 29210 parlnGcprlng 29347

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 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7734 ax-cnex 11227 ax-resscn 11228 ax-1cn 11229 ax-icn 11230 ax-addcl 11231 ax-addrcl 11232 ax-mulcl 11233 ax-mulrcl 11234 ax-mulcom 11235 ax-addass 11236 ax-mulass 11237 ax-distr 11238 ax-i2m1 11239 ax-1ne0 11240 ax-1rid 11241 ax-rnegex 11242 ax-rrecex 11243 ax-cnre 11244 ax-pre-lttri 11245 ax-pre-lttrn 11246 ax-pre-ltadd 11247 ax-pre-mulgt0 11248

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 3739 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 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 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6293 df-ord 6354 df-on 6355 df-lim 6356 df-suc 6357 df-iota 6483 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8454 df-oadd 8458 df-er 8695 df-map 8827 df-pm 8828 df-en 8952 df-dom 8953 df-sdom 8954 df-fin 8955 df-dju 9953 df-card 9991 df-pnf 11316 df-mnf 11317 df-xr 11318 df-ltxr 11319 df-le 11320 df-sub 11514 df-neg 11515 df-nn 12305 df-2 12374 df-3 12375 df-n0 12576 df-xnn0 12649 df-z 12663 df-uz 12935 df-fz 13609 df-fzo 13757 df-hash 14442 df-word 14626 df-concat 14683 df-s1 14710 df-s2 14966 df-s3 14967 df-trkgc 28843 df-trkgb 28844 df-trkgcb 28845 df-trkgld 28847 df-trkg 28848 df-cgrg 28907 df-ismt 28929 df-leg 28979 df-hlg 28997 df-mir 29058 df-rag 29102 df-perpg 29104 df-hpg 29169 df-plng 29185 df-mid 29212 df-lmi 29213 df-cgra 29248 df-prlng 29348

This theorem is used by: symquadprlng 29373 prlngsymquadlem 29374

W3C validator