prlngmid2

Description: If the midpoints of two segments ( X I Z ) and ( Y I W ) coincide, the points X , Y , Z and W form a parallelogram, i.e. the lines ( X L Y ) and ( Z L W ) are parallel. Theorem 12.17 of Schwabhauser p. 125. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	prlngmid2.b	$⊢ P = {Base}_{G}$
	prlngmid2.l	$⊢ L = {Line}_{𝒢} (G)$
	prlngmid2.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	prlngmid2.p	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	prlngmid2.m	$⊢ M = {mid}_{𝒢} (G)$
	prlngmid2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	prlngmid2.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	prlngmid2.x	$⊢ φ \to X \in P$
	prlngmid2.y	$⊢ φ \to Y \in P$
	prlngmid2.z	$⊢ φ \to Z \in (P ∖ (X L Y))$
	prlngmid2.w	$⊢ φ \to W \in P$
	prlngmid2.2	$⊢ φ \to X M Z = Y M W$
	prlngmid2.3	$⊢ φ \to X \neq Y$
Assertion	prlngmid2	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$

Proof

Step	Hyp	Ref	Expression
1		prlngmid2.b	$⊢ P = {Base}_{G}$
2		prlngmid2.l	$⊢ L = {Line}_{𝒢} (G)$
3		prlngmid2.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		prlngmid2.p	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
5		prlngmid2.m	$⊢ M = {mid}_{𝒢} (G)$
6		prlngmid2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
7		prlngmid2.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
8		prlngmid2.x	$⊢ φ \to X \in P$
9		prlngmid2.y	$⊢ φ \to Y \in P$
10		prlngmid2.z	$⊢ φ \to Z \in (P ∖ (X L Y))$
11		prlngmid2.w	$⊢ φ \to W \in P$
12		prlngmid2.2	$⊢ φ \to X M Z = Y M W$
13		prlngmid2.3	$⊢ φ \to X \neq Y$
14	6	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to G \in 𝒢_{Tarski}$
15		eqid	$⊢ Itv (G) = Itv (G)$
16	1 15 2 6 8 9 13	tgelrnln	$⊢ φ \to X L Y \in ran L$
17	1 2 3 6 16 10	tgelrnpln	$⊢ φ \to (X L Y) E Z \in ran E$
18	17	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (X L Y) E Z \in ran E$
19	1 15 2 3 6 16 10	elplnglnid	$⊢ φ \to X L Y \subseteq (X L Y) E Z$
20	19	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X L Y \subseteq (X L Y) E Z$
21	1 15 2 3 6 16 10	elplngid	$⊢ φ \to Z \in ((X L Y) E Z)$
22	12	fveq2d	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) = {pInv}_{𝒢} (G) (Y M W)$
23	22	fveq1d	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) (Y) = {pInv}_{𝒢} (G) (Y M W) (Y)$
24	5	oveqi	$⊢ Y M W = Y {mid}_{𝒢} (G) W$
25	24	eqcomi	$⊢ Y {mid}_{𝒢} (G) W = Y M W$
26		eqid	$⊢ dist (G) = dist (G)$
27	10	eldifad	$⊢ φ \to Z \in P$
28	10	eldifbd	$⊢ φ \to \neg Z \in (X L Y)$
29	13	neneqd	$⊢ φ \to \neg X = Y$
30		ioran	$⊢ \neg (Z \in (X L Y) \lor X = Y) \leftrightarrow (\neg Z \in (X L Y) \land \neg X = Y)$
31	28 29 30	sylanbrc	$⊢ φ \to \neg (Z \in (X L Y) \lor X = Y)$
32	1 2 15 6 8 9 27 31	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
33		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
34	5	oveqi	$⊢ X M Z = X {mid}_{𝒢} (G) Z$
35	1 26 15 6 32 8 27	midcl	$⊢ φ \to X {mid}_{𝒢} (G) Z \in P$
36	34 35	eqeltrid	$⊢ φ \to X M Z \in P$
37	12 36	eqeltrrd	$⊢ φ \to Y M W \in P$
38	1 26 15 6 32 9 11 33 37	ismidb	$⊢ φ \to (W = {pInv}_{𝒢} (G) (Y M W) (Y) \leftrightarrow Y {mid}_{𝒢} (G) W = Y M W)$
39	25 38	mpbiri	$⊢ φ \to W = {pInv}_{𝒢} (G) (Y M W) (Y)$
40	23 39	eqtr4d	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) (Y) = W$
41		eqid	$⊢ {pInv}_{𝒢} (G) (X M Z) = {pInv}_{𝒢} (G) (X M Z)$
42	1 15 2 6 8 9 13	tglinerflx1	$⊢ φ \to X \in (X L Y)$
43	19 42	sseldd	$⊢ φ \to X \in ((X L Y) E Z)$
44		nelne2	$⊢ (X \in (X L Y) \land \neg Z \in (X L Y)) \to X \neq Z$
45	42 28 44	syl2anc	$⊢ φ \to X \neq Z$
46	1 15 2 3 6 17 43 21 45	lnssplng1	$⊢ φ \to X L Z \subseteq (X L Y) E Z$
47	1 26 15 6 32 8 27	midbtwn	$⊢ φ \to X {mid}_{𝒢} (G) Z \in (X Itv (G) Z)$
48	34 47	eqeltrid	$⊢ φ \to X M Z \in (X Itv (G) Z)$
49	1 15 2 6 8 27 36 45 48	btwnlng1	$⊢ φ \to X M Z \in (X L Z)$
50	46 49	sseldd	$⊢ φ \to X M Z \in ((X L Y) E Z)$
51	1 15 2 6 8 9 13	tglinerflx2	$⊢ φ \to Y \in (X L Y)$
52	19 51	sseldd	$⊢ φ \to Y \in ((X L Y) E Z)$
53	1 3 33 41 6 17 50 52	mirplncl	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) (Y) \in ((X L Y) E Z)$
54	40 53	eqeltrrd	$⊢ φ \to W \in ((X L Y) E Z)$
55	6	adantr	$⊢ (φ \land Z = W) \to G \in 𝒢_{Tarski}$
56	36	adantr	$⊢ (φ \land Z = W) \to X M Z \in P$
57	8	adantr	$⊢ (φ \land Z = W) \to X \in P$
58	9	adantr	$⊢ (φ \land Z = W) \to Y \in P$
59	34	eqcomi	$⊢ X {mid}_{𝒢} (G) Z = X M Z$
60	1 26 15 6 32 8 27 33 36	ismidb	$⊢ φ \to (Z = {pInv}_{𝒢} (G) (X M Z) (X) \leftrightarrow X {mid}_{𝒢} (G) Z = X M Z)$
61	59 60	mpbiri	$⊢ φ \to Z = {pInv}_{𝒢} (G) (X M Z) (X)$
62	61	eqcomd	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) (X) = Z$
63	62	adantr	$⊢ (φ \land Z = W) \to {pInv}_{𝒢} (G) (X M Z) (X) = Z$
64		simpr	$⊢ (φ \land Z = W) \to Z = W$
65	40	eqcomd	$⊢ φ \to W = {pInv}_{𝒢} (G) (X M Z) (Y)$
66	65	adantr	$⊢ (φ \land Z = W) \to W = {pInv}_{𝒢} (G) (X M Z) (Y)$
67	63 64 66	3eqtrd	$⊢ (φ \land Z = W) \to {pInv}_{𝒢} (G) (X M Z) (X) = {pInv}_{𝒢} (G) (X M Z) (Y)$
68	1 26 15 2 33 55 56 41 57 58 67	mireq	$⊢ (φ \land Z = W) \to X = Y$
69	13 68	mteqand	$⊢ φ \to Z \neq W$
70	1 15 2 3 6 17 21 54 69	lnssplng1	$⊢ φ \to Z L W \subseteq (X L Y) E Z$
71	70	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to Z L W \subseteq (X L Y) E Z$
72	42	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X \in (X L Y)$
73	20 72	sseldd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X \in ((X L Y) E Z)$
74	21	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to Z \in ((X L Y) E Z)$
75	45	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X \neq Z$
76	1 15 2 3 14 18 73 74 75	lnssplng1	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X L Z \subseteq (X L Y) E Z$
77	49	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X M Z \in (X L Z)$
78	76 77	sseldd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X M Z \in ((X L Y) E Z)$
79		simplr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e \in (X L Y)$
80	20 79	sseldd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e \in ((X L Y) E Z)$
81	6	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to G \in 𝒢_{Tarski}$
82	8	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X \in P$
83	36	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X M Z \in P$
84	27	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to Z \in P$
85		simpr	$⊢ (φ \land X = X M Z) \to X = X M Z$
86	85 34	eqtr2di	$⊢ (φ \land X = X M Z) \to X {mid}_{𝒢} (G) Z = X$
87	1 26 15 6 32 8 27 33 8	ismidb	$⊢ φ \to (Z = {pInv}_{𝒢} (G) (X) (X) \leftrightarrow X {mid}_{𝒢} (G) Z = X)$
88	87	adantr	$⊢ (φ \land X = X M Z) \to (Z = {pInv}_{𝒢} (G) (X) (X) \leftrightarrow X {mid}_{𝒢} (G) Z = X)$
89	86 88	mpbird	$⊢ (φ \land X = X M Z) \to Z = {pInv}_{𝒢} (G) (X) (X)$
90		eqid	$⊢ {pInv}_{𝒢} (G) (X) = {pInv}_{𝒢} (G) (X)$
91	1 26 15 2 33 6 8 90	mircinv	$⊢ φ \to {pInv}_{𝒢} (G) (X) (X) = X$
92	91	adantr	$⊢ (φ \land X = X M Z) \to {pInv}_{𝒢} (G) (X) (X) = X$
93	89 92	eqtr2d	$⊢ (φ \land X = X M Z) \to X = Z$
94	42	adantr	$⊢ (φ \land X = X M Z) \to X \in (X L Y)$
95	93 94	eqeltrrd	$⊢ (φ \land X = X M Z) \to Z \in (X L Y)$
96	28 95	mtand	$⊢ φ \to \neg X = X M Z$
97	96	neqned	$⊢ φ \to X \neq X M Z$
98	97	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X \neq X M Z$
99	1 15 2 6 8 27 45	tglinecom	$⊢ φ \to X L Z = Z L X$
100	49 99	eleqtrd	$⊢ φ \to X M Z \in (Z L X)$
101	100	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X M Z \in (Z L X)$
102	45	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X \neq Z$
103	102	necomd	$⊢ (φ \land X M Z \in (X L Y)) \to Z \neq X$
104	1 15 2 81 82 83 84 98 101 103	lnrot1	$⊢ (φ \land X M Z \in (X L Y)) \to Z \in (X L (X M Z))$
105	16	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X L Y \in ran L$
106	42	adantr	$⊢ (φ \land X M Z \in (X L Y)) \to X \in (X L Y)$
107		simpr	$⊢ (φ \land X M Z \in (X L Y)) \to X M Z \in (X L Y)$
108	1 15 2 81 82 83 98 98 105 106 107	tglinethru	$⊢ (φ \land X M Z \in (X L Y)) \to X L Y = X L (X M Z)$
109	104 108	eleqtrrd	$⊢ (φ \land X M Z \in (X L Y)) \to Z \in (X L Y)$
110	28 109	mtand	$⊢ φ \to \neg X M Z \in (X L Y)$
111	110	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to \neg X M Z \in (X L Y)$
112		nelne2	$⊢ (e \in (X L Y) \land \neg X M Z \in (X L Y)) \to e \neq X M Z$
113	79 111 112	syl2anc	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e \neq X M Z$
114	113	necomd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X M Z \neq e$
115	1 15 2 3 14 18 78 80 114	lnssplng1	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (X M Z) L e \subseteq (X L Y) E Z$
116	16	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X L Y \in ran L$
117	1 2 15 14 116 79	tglnpt	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e \in P$
118	36	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X M Z \in P$
119	1 15 2 14 117 118 113	tglinecom	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e L (X M Z) = (X M Z) L e$
120	1 15 2 14 117 118 113	tgelrnln	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e L (X M Z) \in ran L$
121		simpr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)$
122	119 121	eqbrtrd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (e L (X M Z)) ⟂_{𝒢} (G) (X L Y)$
123	1 26 15 2 14 120 116 122	perpcom	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (X L Y) ⟂_{𝒢} (G) (e L (X M Z))$
124	119 123	breq2dd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (X L Y) ⟂_{𝒢} (G) ((X M Z) L e)$
125	14	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to G \in 𝒢_{Tarski}$
126	1 15 2 6 27 11 69	tgelrnln	$⊢ φ \to Z L W \in ran L$
127	126	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to Z L W \in ran L$
128	127	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to Z L W \in ran L$
129	119 120	eqeltrrd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (X M Z) L e \in ran L$
130	129	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to (X M Z) L e \in ran L$
131		simpr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to Z = {pInv}_{𝒢} (G) (X M Z) (e)$
132	8	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X \in P$
133	9	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to Y \in P$
134	13	necomd	$⊢ φ \to Y \neq X$
135	134	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to Y \neq X$
136	1 2 33 41 14 118 117 132 133 135 79	mirlni	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (e) \in ({pInv}_{𝒢} (G) (X M Z) (X) L {pInv}_{𝒢} (G) (X M Z) (Y))$
137	62 40	oveq12d	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) (X) L {pInv}_{𝒢} (G) (X M Z) (Y) = Z L W$
138	137	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (X) L {pInv}_{𝒢} (G) (X M Z) (Y) = Z L W$
139	136 138	eleqtrd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (e) \in (Z L W)$
140	1 15 2 14 118 117 114	tglinerflx1	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X M Z \in ((X M Z) L e)$
141	1 15 2 14 118 117 114	tglinerflx2	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e \in ((X M Z) L e)$
142	1 26 15 2 33 14 41 129 140 141	mirln	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (e) \in ((X M Z) L e)$
143	139 142	elind	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (e) \in ((Z L W) \cap ((X M Z) L e))$
144	143	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to {pInv}_{𝒢} (G) (X M Z) (e) \in ((Z L W) \cap ((X M Z) L e))$
145	131 144	eqeltrd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to Z \in ((Z L W) \cap ((X M Z) L e))$
146	1 15 2 6 27 11 69	tglinerflx2	$⊢ φ \to W \in (Z L W)$
147	146	ad3antrrr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to W \in (Z L W)$
148	140	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X M Z \in ((X M Z) L e)$
149	69	necomd	$⊢ φ \to W \neq Z$
150	149	ad3antrrr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to W \neq Z$
151	1 26 15 2 33 14 118 41 117 113	mirne	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (e) \neq X M Z$
152	151	necomd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to X M Z \neq {pInv}_{𝒢} (G) (X M Z) (e)$
153	152	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X M Z \neq {pInv}_{𝒢} (G) (X M Z) (e)$
154	153 131	neeqtrrd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X M Z \neq Z$
155	40	ad3antrrr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to {pInv}_{𝒢} (G) (X M Z) (Y) = W$
156	131	eqcomd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to {pInv}_{𝒢} (G) (X M Z) (e) = Z$
157	1 26 15 2 33 6 36 41	mircinv	$⊢ φ \to {pInv}_{𝒢} (G) (X M Z) (X M Z) = X M Z$
158	157	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (X M Z) = X M Z$
159	158	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to {pInv}_{𝒢} (G) (X M Z) (X M Z) = X M Z$
160	155 156 159	s3eqd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to ⟨“ {pInv}_{𝒢} (G) (X M Z) (Y) {pInv}_{𝒢} (G) (X M Z) (e) {pInv}_{𝒢} (G) (X M Z) (X M Z) ”⟩ = ⟨“ W Z (X M Z) ”⟩$
161	133	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to Y \in P$
162	117	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to e \in P$
163	118	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X M Z \in P$
164	132	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X \in P$
165	1 15 2 14 133 132 117 135 79	lncom	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to e \in (Y L X)$
166	165	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to e \in (Y L X)$
167	1 15 2 6 8 9 13	tglinecom	$⊢ φ \to X L Y = Y L X$
168	167	ad3antrrr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X L Y = Y L X$
169	116	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to X L Y \in ran L$
170		simplr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)$
171	1 26 15 2 125 130 169 170	perpcom	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to (X L Y) ⟂_{𝒢} (G) ((X M Z) L e)$
172	168 171	eqbrtrrd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to (Y L X) ⟂_{𝒢} (G) ((X M Z) L e)$
173	119	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to e L (X M Z) = (X M Z) L e$
174	172 173	breqtrrd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to (Y L X) ⟂_{𝒢} (G) (e L (X M Z))$
175	1 26 15 2 125 161 164 166 163 174	perprag	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to ⟨“ Y e (X M Z) ”⟩ \in ∟_{𝒢} (G)$
176	1 26 15 2 33 125 161 162 163 175 41 163	mirrag	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to ⟨“ {pInv}_{𝒢} (G) (X M Z) (Y) {pInv}_{𝒢} (G) (X M Z) (e) {pInv}_{𝒢} (G) (X M Z) (X M Z) ”⟩ \in ∟_{𝒢} (G)$
177	160 176	eqeltrrd	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to ⟨“ W Z (X M Z) ”⟩ \in ∟_{𝒢} (G)$
178	1 26 15 2 125 128 130 145 147 148 150 154 177	ragperp	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z = {pInv}_{𝒢} (G) (X M Z) (e)) \to (Z L W) ⟂_{𝒢} (G) ((X M Z) L e)$
179	14	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to G \in 𝒢_{Tarski}$
180	127	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to Z L W \in ran L$
181	129	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to (X M Z) L e \in ran L$
182	143	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to {pInv}_{𝒢} (G) (X M Z) (e) \in ((Z L W) \cap ((X M Z) L e))$
183	1 15 2 6 27 11 69	tglinerflx1	$⊢ φ \to Z \in (Z L W)$
184	183	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to Z \in (Z L W)$
185	184	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to Z \in (Z L W)$
186	140	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to X M Z \in ((X M Z) L e)$
187		simpr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to Z \neq {pInv}_{𝒢} (G) (X M Z) (e)$
188	152	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to X M Z \neq {pInv}_{𝒢} (G) (X M Z) (e)$
189	62	ad2antrr	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (X) = Z$
190		eqidd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to {pInv}_{𝒢} (G) (X M Z) (e) = {pInv}_{𝒢} (G) (X M Z) (e)$
191	189 190 158	s3eqd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to ⟨“ {pInv}_{𝒢} (G) (X M Z) (X) {pInv}_{𝒢} (G) (X M Z) (e) {pInv}_{𝒢} (G) (X M Z) (X M Z) ”⟩ = ⟨“ Z {pInv}_{𝒢} (G) (X M Z) (e) (X M Z) ”⟩$
192	1 26 15 2 14 132 133 79 118 123	perprag	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to ⟨“ X e (X M Z) ”⟩ \in ∟_{𝒢} (G)$
193	1 26 15 2 33 14 132 117 118 192 41 118	mirrag	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to ⟨“ {pInv}_{𝒢} (G) (X M Z) (X) {pInv}_{𝒢} (G) (X M Z) (e) {pInv}_{𝒢} (G) (X M Z) (X M Z) ”⟩ \in ∟_{𝒢} (G)$
194	191 193	eqeltrrd	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to ⟨“ Z {pInv}_{𝒢} (G) (X M Z) (e) (X M Z) ”⟩ \in ∟_{𝒢} (G)$
195	194	adantr	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to ⟨“ Z {pInv}_{𝒢} (G) (X M Z) (e) (X M Z) ”⟩ \in ∟_{𝒢} (G)$
196	1 26 15 2 179 180 181 182 185 186 187 188 195	ragperp	$⊢ (((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \land Z \neq {pInv}_{𝒢} (G) (X M Z) (e)) \to (Z L W) ⟂_{𝒢} (G) ((X M Z) L e)$
197	178 196	pm2.61dane	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (Z L W) ⟂_{𝒢} (G) ((X M Z) L e)$
198	1 2 3 4 14 18 20 71 115 124 197	perpprlng	$⊢ ((φ \land e \in (X L Y)) \land ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)) \to (X L Y) \underset{˙}{∥} (Z L W)$
199	1 26 15 2 6 16 36 110	footex	$⊢ φ \to \exists e \in (X L Y) ((X M Z) L e) ⟂_{𝒢} (G) (X L Y)$
200	198 199	r19.29a	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$

Metamath Proof Explorer

Theorem prlngmid2

Proof