Theorem symquadprlng

Description: Symmetrical quadrilaterals are parallelograms. Theorem 12.18 of Schwabhauser p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	symquadprlng.p	$$⊢P={\mathrm{Base}}_G$$
	symquadprlng.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	symquadprlng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
	symquadprlng.r	No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
	symquadprlng.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	symquadprlng.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
	symquadprlng.x	$$⊢\phi \to X\in P$$
	symquadprlng.y	$$⊢\phi \to Y\in P$$
	symquadprlng.z	$$⊢\phi \to Z\in P$$
	symquadprlng.w	$$⊢\phi \to W\in P$$
	symquadprlng.2	$$⊢\phi \to X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}W$$
	symquadprlng.3	$$⊢\phi \to Y\underset{\dot{}}{-}Z=W\underset{\dot{}}{-}X$$
	symquadprlng.4	$$⊢\phi \to \neg \left(X\in \left(YLZ\right)\vee Y=Z\right)$$
	symquadprlng.5	$$⊢\phi \to Y\ne W$$
	symquadprlng.6	$$⊢\phi \to T\in \left(XLZ\right)$$
	symquadprlng.7	$$⊢\phi \to T\in \left(YLW\right)$$
Assertion	symquadprlng	$$⊢\phi \to \left(\left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)\wedge \left(YLZ\right)\underset{\dot{}}{\parallel }\left(WLX\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		symquadprlng.p	$$⊢P={\mathrm{Base}}_G$$
2		symquadprlng.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		symquadprlng.l	$$⊢L={Line}_{𝒢}\left(G\right)$$
4		symquadprlng.r	Could not format .|| = ( parlnG ` G ) : No typesetting found for |- .|| = ( parlnG ` G ) with typecode |-
5		symquadprlng.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		symquadprlng.1	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^E$$
7		symquadprlng.x	$$⊢\phi \to X\in P$$
8		symquadprlng.y	$$⊢\phi \to Y\in P$$
9		symquadprlng.z	$$⊢\phi \to Z\in P$$
10		symquadprlng.w	$$⊢\phi \to W\in P$$
11		symquadprlng.2	$$⊢\phi \to X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}W$$
12		symquadprlng.3	$$⊢\phi \to Y\underset{\dot{}}{-}Z=W\underset{\dot{}}{-}X$$
13		symquadprlng.4	$$⊢\phi \to \neg \left(X\in \left(YLZ\right)\vee Y=Z\right)$$
14		symquadprlng.5	$$⊢\phi \to Y\ne W$$
15		symquadprlng.6	$$⊢\phi \to T\in \left(XLZ\right)$$
16		symquadprlng.7	$$⊢\phi \to T\in \left(YLW\right)$$
17		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for |- ( PlnG ` G ) = ( PlnG ` G ) with typecode |-
18		eqid	$$⊢{mid}_{𝒢}\left(G\right)={mid}_{𝒢}\left(G\right)$$
19		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
20	1 3 19 5 8 9 7 13	ncolrot2	$$⊢\phi \to \neg \left(Z\in \left(XLY\right)\vee X=Y\right)$$
21	20	orsild	$$⊢\phi \to \neg Z\in \left(XLY\right)$$
22	9 21	eldifd	$$⊢\phi \to Z\in \left(P\setminus \left(XLY\right)\right)$$
23		eqid	$$⊢{pInv}_{𝒢}\left(G\right)={pInv}_{𝒢}\left(G\right)$$
24		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(T\right)={pInv}_{𝒢}\left(G\right)\left(T\right)$$
25	1 19 3 5 8 10 14	tgelrnln	$$⊢\phi \to YLW\in \mathrm{ran}L$$
26	1 3 19 5 25 16	tglnpt	$$⊢\phi \to T\in P$$
27	15	orcd	$$⊢\phi \to \left(T\in \left(XLZ\right)\vee X=Z\right)$$
28	16	orcd	$$⊢\phi \to \left(T\in \left(YLW\right)\vee Y=W\right)$$
29	1 2 19 3 23 5 24 7 8 9 10 26 13 14 11 12 27 28	symquadlem	$$⊢\phi \to X={pInv}_{𝒢}\left(G\right)\left(T\right)\left(Z\right)$$
30	1 3 19 5 8 9 7 13	ncoltgdim2	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
31	1 2 19 5 30 9 7 23 26	ismidb	$$⊢\phi \to \left(X={pInv}_{𝒢}\left(G\right)\left(T\right)\left(Z\right)\leftrightarrow Z{mid}_{𝒢}\left(G\right)X=T\right)$$
32	29 31	mpbid	$$⊢\phi \to Z{mid}_{𝒢}\left(G\right)X=T$$
33	1 2 19 5 30 7 9	midcom	$$⊢\phi \to X{mid}_{𝒢}\left(G\right)Z=Z{mid}_{𝒢}\left(G\right)X$$
34	1 2 3 5 7 8 9 10 11 12 13 14 15 16	symquadprlnglem	$$⊢\phi \to \neg \left(W\in \left(ZLY\right)\vee Z=Y\right)$$
35	1 3 19 5 7 9 15	tglngne	$$⊢\phi \to X\ne Z$$
36	35	necomd	$$⊢\phi \to Z\ne X$$
37	1 2 19 5 7 8 9 10 11	tgcgrcomlr	$$⊢\phi \to Y\underset{\dot{}}{-}X=W\underset{\dot{}}{-}Z$$
38	37	eqcomd	$$⊢\phi \to W\underset{\dot{}}{-}Z=Y\underset{\dot{}}{-}X$$
39	1 2 19 5 8 9 10 7 12	tgcgrcomlr	$$⊢\phi \to Z\underset{\dot{}}{-}Y=X\underset{\dot{}}{-}W$$
40	1 3 19 5 8 10 26 28	colcom	$$⊢\phi \to \left(T\in \left(WLY\right)\vee W=Y\right)$$
41	1 3 19 5 7 9 26 27	colcom	$$⊢\phi \to \left(T\in \left(ZLX\right)\vee Z=X\right)$$
42	1 2 19 3 23 5 24 10 9 8 7 26 34 36 38 39 40 41	symquadlem	$$⊢\phi \to W={pInv}_{𝒢}\left(G\right)\left(T\right)\left(Y\right)$$
43	1 2 19 5 30 8 10 23 26	ismidb	$$⊢\phi \to \left(W={pInv}_{𝒢}\left(G\right)\left(T\right)\left(Y\right)\leftrightarrow Y{mid}_{𝒢}\left(G\right)W=T\right)$$
44	42 43	mpbid	$$⊢\phi \to Y{mid}_{𝒢}\left(G\right)W=T$$
45	32 33 44	3eqtr4d	$$⊢\phi \to X{mid}_{𝒢}\left(G\right)Z=Y{mid}_{𝒢}\left(G\right)W$$
46	1 19 3 5 7 8 9 13	ncolne1	$$⊢\phi \to X\ne Y$$
47	1 3 17 4 18 5 6 7 8 22 10 45 46	prlngmid2	$$⊢\phi \to \left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)$$
48	34	orsild	$$⊢\phi \to \neg W\in \left(ZLY\right)$$
49	34	orsird	$$⊢\phi \to \neg Z=Y$$
50	49	neqned	$$⊢\phi \to Z\ne Y$$
51	1 19 3 5 9 8 50	tglinecom	$$⊢\phi \to ZLY=YLZ$$
52	48 51	neleqtrd	$$⊢\phi \to \neg W\in \left(YLZ\right)$$
53	10 52	eldifd	$$⊢\phi \to W\in \left(P\setminus \left(YLZ\right)\right)$$
54	44 32	eqtr4d	$$⊢\phi \to Y{mid}_{𝒢}\left(G\right)W=Z{mid}_{𝒢}\left(G\right)X$$
55	50	necomd	$$⊢\phi \to Y\ne Z$$
56	1 3 17 4 18 5 6 8 9 53 7 54 55	prlngmid2	$$⊢\phi \to \left(YLZ\right)\underset{\dot{}}{\parallel }\left(WLX\right)$$
57	47 56	jca	$$⊢\phi \to \left(\left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)\wedge \left(YLZ\right)\underset{\dot{}}{\parallel }\left(WLX\right)\right)$$