prlngsymquadopp

Description: In parallelograms, opposing vertices are on opposite sides of the diagonal. Second part of Theorem 12.19 of Schwabhauser p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	symquadprlng.p	$⊢ P = {Base}_{G}$
	symquadprlng.d	$⊢ \underset{˙}{-} = dist (G)$
	symquadprlng.l	$⊢ L = {Line}_{𝒢} (G)$
	symquadprlng.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	symquadprlng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	symquadprlng.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	symquadprlng.x	$⊢ φ \to X \in P$
	symquadprlng.y	$⊢ φ \to Y \in P$
	symquadprlng.z	$⊢ φ \to Z \in P$
	symquadprlng.w	$⊢ φ \to W \in P$
	prlngsymquad.2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
	prlngsymquad.3	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$
	prlngsymquad.4	$⊢ φ \to (Y L Z) \underset{˙}{∥} (W L X)$
	prlngsymquadopp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\}$
	prlngsymquadopp.i	$⊢ I = Itv (G)$
Assertion	prlngsymquadopp	$⊢ φ \to W O Y$

Proof

Step	Hyp	Ref	Expression
1		symquadprlng.p	$⊢ P = {Base}_{G}$
2		symquadprlng.d	$⊢ \underset{˙}{-} = dist (G)$
3		symquadprlng.l	$⊢ L = {Line}_{𝒢} (G)$
4		symquadprlng.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
5		symquadprlng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		symquadprlng.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
7		symquadprlng.x	$⊢ φ \to X \in P$
8		symquadprlng.y	$⊢ φ \to Y \in P$
9		symquadprlng.z	$⊢ φ \to Z \in P$
10		symquadprlng.w	$⊢ φ \to W \in P$
11		prlngsymquad.2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
12		prlngsymquad.3	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$
13		prlngsymquad.4	$⊢ φ \to (Y L Z) \underset{˙}{∥} (W L X)$
14		prlngsymquadopp.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Z)) \land b \in (P ∖ (X L Z))) \land \exists t \in (X L Z) t \in (a I b))\}$
15		prlngsymquadopp.i	$⊢ I = Itv (G)$
16	1 3 15 5 8 9 7 11	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
17	1 2 15 5 16 7 9	midcl	$⊢ φ \to X {mid}_{𝒢} (G) Z \in P$
18	1 15 3 5 7 8 9 11	ncolne2	$⊢ φ \to X \neq Z$
19	1 2 15 5 16 7 9	midbtwn	$⊢ φ \to X {mid}_{𝒢} (G) Z \in (X I Z)$
20	1 15 3 5 7 9 17 18 19	btwnlng1	$⊢ φ \to X {mid}_{𝒢} (G) Z \in (X L Z)$
21	1 3 15 5 8 9 7 11	ncolcom	$⊢ φ \to \neg (X \in (Z L Y) \lor Z = Y)$
22	1 3 15 5 9 8 7 21	ncolrot2	$⊢ φ \to \neg (Y \in (X L Z) \lor X = Z)$
23	22	orsild	$⊢ φ \to \neg Y \in (X L Z)$
24	1 15 3 5 8 7 9 22	ncolne2	$⊢ φ \to Y \neq Z$
25	1 15 3 5 8 9 24	tglinerflx1	$⊢ φ \to Y \in (Y L Z)$
26	25	adantr	$⊢ (φ \land W \in (X L Z)) \to Y \in (Y L Z)$
27	5	adantr	$⊢ (φ \land W \in (X L Z)) \to G \in 𝒢_{Tarski}$
28	6	adantr	$⊢ (φ \land W \in (X L Z)) \to G \in 𝒢_{Tarski}^{E}$
29	13	adantr	$⊢ (φ \land W \in (X L Z)) \to (Y L Z) \underset{˙}{∥} (W L X)$
30	7	adantr	$⊢ (φ \land W \in (X L Z)) \to X \in P$
31	10	adantr	$⊢ (φ \land W \in (X L Z)) \to W \in P$
32	3 4 5 13	prlngrcl2	$⊢ φ \to W L X \in ran L$
33	1 15 3 5 10 7 32	tglnne	$⊢ φ \to W \neq X$
34	33	necomd	$⊢ φ \to X \neq W$
35	34	adantr	$⊢ (φ \land W \in (X L Z)) \to X \neq W$
36	9	adantr	$⊢ (φ \land W \in (X L Z)) \to Z \in P$
37	18	adantr	$⊢ (φ \land W \in (X L Z)) \to X \neq Z$
38	37	necomd	$⊢ (φ \land W \in (X L Z)) \to Z \neq X$
39		simpr	$⊢ (φ \land W \in (X L Z)) \to W \in (X L Z)$
40	1 15 3 27 30 36 37	tglinecom	$⊢ (φ \land W \in (X L Z)) \to X L Z = Z L X$
41	39 40	eleqtrd	$⊢ (φ \land W \in (X L Z)) \to W \in (Z L X)$
42	1 15 3 27 30 31 36 35 41 38	lnrot1	$⊢ (φ \land W \in (X L Z)) \to Z \in (X L W)$
43	1 15 3 27 30 31 35 36 38 42	tglineelsb2	$⊢ (φ \land W \in (X L Z)) \to X L W = X L Z$
44	1 15 3 5 7 10 34	tglinecom	$⊢ φ \to X L W = W L X$
45	44	adantr	$⊢ (φ \land W \in (X L Z)) \to X L W = W L X$
46	43 45	eqtr3d	$⊢ (φ \land W \in (X L Z)) \to X L Z = W L X$
47	29 46	breqtrrd	$⊢ (φ \land W \in (X L Z)) \to (Y L Z) \underset{˙}{∥} (X L Z)$
48		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for \|- ( PlnG ` G ) = ( PlnG ` G ) with typecode \|-
49	3 4 5 13	prlngrcl1	$⊢ φ \to Y L Z \in ran L$
50	3 48 4 5 49	prlngref	$⊢ φ \to (Y L Z) \underset{˙}{∥} (Y L Z)$
51	50	adantr	$⊢ (φ \land W \in (X L Z)) \to (Y L Z) \underset{˙}{∥} (Y L Z)$
52	42 43	eleqtrd	$⊢ (φ \land W \in (X L Z)) \to Z \in (X L Z)$
53	1 15 3 5 8 9 24	tglinerflx2	$⊢ φ \to Z \in (Y L Z)$
54	53	adantr	$⊢ (φ \land W \in (X L Z)) \to Z \in (Y L Z)$
55	1 4 27 28 47 51 52 54	prlngeq	$⊢ (φ \land W \in (X L Z)) \to X L Z = Y L Z$
56	26 55	eleqtrrd	$⊢ (φ \land W \in (X L Z)) \to Y \in (X L Z)$
57	23 56	mtand	$⊢ φ \to \neg W \in (X L Z)$
58		eqid	$⊢ {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y)$
59	1 2 3 4 5 6 7 8 9 10 11 12 13 58	prlngsymquadlem	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) = W$
60	59	eqcomd	$⊢ φ \to W = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y)$
61		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
62	1 2 15 5 16 8 10 61 17	ismidb	$⊢ φ \to (W = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) \leftrightarrow Y {mid}_{𝒢} (G) W = X {mid}_{𝒢} (G) Z)$
63	60 62	mpbid	$⊢ φ \to Y {mid}_{𝒢} (G) W = X {mid}_{𝒢} (G) Z$
64	1 2 15 5 16 8 10	midcl	$⊢ φ \to Y {mid}_{𝒢} (G) W \in P$
65	1 2 15 5 16 8 10	midbtwn	$⊢ φ \to Y {mid}_{𝒢} (G) W \in (Y I W)$
66	1 2 15 5 8 64 10 65	tgbtwncom	$⊢ φ \to Y {mid}_{𝒢} (G) W \in (W I Y)$
67	63 66	eqeltrrd	$⊢ φ \to X {mid}_{𝒢} (G) Z \in (W I Y)$
68	1 2 15 14 10 8 20 57 23 67	islnoppd	$⊢ φ \to W O Y$

Metamath Proof Explorer

Theorem prlngsymquadopp

Proof