Theorem prlngsymquad

Description: All parallelograms are symmetric quadrilaterals. First part of Theorem 12.19 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$$
	prlngsymquad.2	$$⊢\phi \to \neg \left(X\in \left(YLZ\right)\vee Y=Z\right)$$
	prlngsymquad.3	$$⊢\phi \to \left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)$$
	prlngsymquad.4	$$⊢\phi \to \left(YLZ\right)\underset{\dot{}}{\parallel }\left(WLX\right)$$
Assertion	prlngsymquad	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}W\wedge Y\underset{\dot{}}{-}Z=W\underset{\dot{}}{-}X\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		prlngsymquad.2	$$⊢\phi \to \neg \left(X\in \left(YLZ\right)\vee Y=Z\right)$$
12		prlngsymquad.3	$$⊢\phi \to \left(XLY\right)\underset{\dot{}}{\parallel }\left(ZLW\right)$$
13		prlngsymquad.4	$$⊢\phi \to \left(YLZ\right)\underset{\dot{}}{\parallel }\left(WLX\right)$$
14		eqidd	$$⊢\phi \to X{mid}_{𝒢}\left(G\right)Z=X{mid}_{𝒢}\left(G\right)Z$$
15		eqid	$$⊢\mathrm{Itv}\left(G\right)=\mathrm{Itv}\left(G\right)$$
16	1 3 15 5 8 9 7 11	ncoltgdim2	$$⊢\phi \to G{\mathrm{Dim}}_{𝒢}\ge 2$$
17		eqid	$$⊢{pInv}_{𝒢}\left(G\right)={pInv}_{𝒢}\left(G\right)$$
18	1 2 15 5 16 7 9	midcl	$$⊢\phi \to X{mid}_{𝒢}\left(G\right)Z\in P$$
19	1 2 15 5 16 7 9 17 18	ismidb	$$⊢\phi \to \left(Z={pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(X\right)\leftrightarrow X{mid}_{𝒢}\left(G\right)Z=X{mid}_{𝒢}\left(G\right)Z\right)$$
20	14 19	mpbird	$$⊢\phi \to Z={pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(X\right)$$
21	20	eqcomd	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(X\right)=Z$$
22	21	oveq1d	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(X\right)\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)=Z\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)$$
23		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)={pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)$$
24	1 2 15 3 17 5 18 23 7 8	miriso	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(X\right)\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)=X\underset{\dot{}}{-}Y$$
25		eqid	$$⊢{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)={pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)$$
26	1 2 3 4 5 6 7 8 9 10 11 12 13 25	prlngsymquadlem	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)=W$$
27	26	oveq2d	$$⊢\phi \to Z\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)=Z\underset{\dot{}}{-}W$$
28	22 24 27	3eqtr3d	$$⊢\phi \to X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}W$$
29	1 2 15 3 17 5 18 23 7 21	mircom	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Z\right)=X$$
30	29	oveq2d	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Z\right)={pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)\underset{\dot{}}{-}X$$
31	1 2 15 3 17 5 18 23 8 9	miriso	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)\underset{\dot{}}{-}{pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Z\right)=Y\underset{\dot{}}{-}Z$$
32	26	oveq1d	$$⊢\phi \to {pInv}_{𝒢}\left(G\right)\left(X{mid}_{𝒢}\left(G\right)Z\right)\left(Y\right)\underset{\dot{}}{-}X=W\underset{\dot{}}{-}X$$
33	30 31 32	3eqtr3d	$$⊢\phi \to Y\underset{\dot{}}{-}Z=W\underset{\dot{}}{-}X$$
34	28 33	jca	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y=Z\underset{\dot{}}{-}W\wedge Y\underset{\dot{}}{-}Z=W\underset{\dot{}}{-}X\right)$$