Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	symquadprlng.d	⊢ − = ( dist ‘ 𝐺 )
	symquadprlng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	symquadprlng.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
	symquadprlng.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	symquadprlng.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
	symquadprlng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	symquadprlng.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	symquadprlng.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	symquadprlng.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	prlngsymquad.2	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
	prlngsymquad.3	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
	prlngsymquad.4	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
	prlngsymquadopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
	prlngsymquadopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	prlngsymquadopp	⊢ ( 𝜑 → 𝑊 𝑂 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		symquadprlng.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		symquadprlng.d	⊢ − = ( dist ‘ 𝐺 )
3		symquadprlng.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		symquadprlng.r	⊢ ∥ = ( parlnG ‘ 𝐺 )
5		symquadprlng.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		symquadprlng.1	⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
7		symquadprlng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
8		symquadprlng.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
9		symquadprlng.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
10		symquadprlng.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
11		prlngsymquad.2	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
12		prlngsymquad.3	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∥ ( 𝑍 𝐿 𝑊 ) )
13		prlngsymquad.4	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
14		prlngsymquadopp.o	⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑍 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑋 𝐿 𝑍 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
15		prlngsymquadopp.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
16	1 3 15 5 8 9 7 11	ncoltgdim2	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
17	1 2 15 5 16 7 9	midcl	⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ 𝑃 )
18	1 15 3 5 7 8 9 11	ncolne2	⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
19	1 2 15 5 16 7 9	midbtwn	⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ ( 𝑋 𝐼 𝑍 ) )
20	1 15 3 5 7 9 17 18 19	btwnlng1	⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ ( 𝑋 𝐿 𝑍 ) )
21	1 3 15 5 8 9 7 11	ncolcom	⊢ ( 𝜑 → ¬ ( 𝑋 ∈ ( 𝑍 𝐿 𝑌 ) ∨ 𝑍 = 𝑌 ) )
22	1 3 15 5 9 8 7 21	ncolrot2	⊢ ( 𝜑 → ¬ ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
23	22	orsild	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) )
24	1 15 3 5 8 7 9 22	ncolne2	⊢ ( 𝜑 → 𝑌 ≠ 𝑍 )
25	1 15 3 5 8 9 24	tglinerflx1	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) )
27	5	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝐺 ∈ TarskiG )
28	6	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝐺 ∈ TarskiGE )
29	13	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑊 𝐿 𝑋 ) )
30	7	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑋 ∈ 𝑃 )
31	10	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑊 ∈ 𝑃 )
32	3 4 5 13	prlngrcl2	⊢ ( 𝜑 → ( 𝑊 𝐿 𝑋 ) ∈ ran 𝐿 )
33	1 15 3 5 10 7 32	tglnne	⊢ ( 𝜑 → 𝑊 ≠ 𝑋 )
34	33	necomd	⊢ ( 𝜑 → 𝑋 ≠ 𝑊 )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑋 ≠ 𝑊 )
36	9	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑍 ∈ 𝑃 )
37	18	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑋 ≠ 𝑍 )
38	37	necomd	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑍 ≠ 𝑋 )
39		simpr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) )
40	1 15 3 27 30 36 37	tglinecom	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
41	39 40	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑊 ∈ ( 𝑍 𝐿 𝑋 ) )
42	1 15 3 27 30 31 36 35 41 38	lnrot1	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑊 ) )
43	1 15 3 27 30 31 35 36 38 42	tglineelsb2	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑋 𝐿 𝑊 ) = ( 𝑋 𝐿 𝑍 ) )
44	1 15 3 5 7 10 34	tglinecom	⊢ ( 𝜑 → ( 𝑋 𝐿 𝑊 ) = ( 𝑊 𝐿 𝑋 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑋 𝐿 𝑊 ) = ( 𝑊 𝐿 𝑋 ) )
46	43 45	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑋 𝐿 𝑍 ) = ( 𝑊 𝐿 𝑋 ) )
47	29 46	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑋 𝐿 𝑍 ) )
48		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
49	3 4 5 13	prlngrcl1	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
50	3 48 4 5 49	prlngref	⊢ ( 𝜑 → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑌 𝐿 𝑍 ) )
51	50	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑌 𝐿 𝑍 ) ∥ ( 𝑌 𝐿 𝑍 ) )
52	42 43	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) )
53	1 15 3 5 8 9 24	tglinerflx2	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
55	1 4 27 28 47 51 52 54	prlngeq	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → ( 𝑋 𝐿 𝑍 ) = ( 𝑌 𝐿 𝑍 ) )
56	26 55	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) )
57	23 56	mtand	⊢ ( 𝜑 → ¬ 𝑊 ∈ ( 𝑋 𝐿 𝑍 ) )
58		eqid	⊢ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 )
59	1 2 3 4 5 6 7 8 9 10 11 12 13 58	prlngsymquadlem	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) = 𝑊 )
60	59	eqcomd	⊢ ( 𝜑 → 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) )
61		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
62	1 2 15 5 16 8 10 61 17	ismidb	⊢ ( 𝜑 → ( 𝑊 = ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) ‘ 𝑌 ) ↔ ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ) )
63	60 62	mpbid	⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) = ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) )
64	1 2 15 5 16 8 10	midcl	⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) ∈ 𝑃 )
65	1 2 15 5 16 8 10	midbtwn	⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) ∈ ( 𝑌 𝐼 𝑊 ) )
66	1 2 15 5 8 64 10 65	tgbtwncom	⊢ ( 𝜑 → ( 𝑌 ( midG ‘ 𝐺 ) 𝑊 ) ∈ ( 𝑊 𝐼 𝑌 ) )
67	63 66	eqeltrrd	⊢ ( 𝜑 → ( 𝑋 ( midG ‘ 𝐺 ) 𝑍 ) ∈ ( 𝑊 𝐼 𝑌 ) )
68	1 2 15 14 10 8 20 57 23 67	islnoppd	⊢ ( 𝜑 → 𝑊 𝑂 𝑌 )