quadcgrprlng

Description: Nontrivial quadrilaterals with congruent and parallel opposite sides are parallelograms. Theorem 12.20 of Schwabhauser p. 126. (Contributed by Thierry Arnoux, 20-Jul-2026)

	Ref	Expression
Hypotheses	quadcgrprlng.p	$⊢ P = {Base}_{G}$
	quadcgrprlng.d	$⊢ \underset{˙}{-} = dist (G)$
	quadcgrprlng.i	$⊢ I = Itv (G)$
	quadcgrprlng.l	$⊢ L = {Line}_{𝒢} (G)$
	quadcgrprlng.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	quadcgrprlng.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))\}$
	quadcgrprlng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	quadcgrprlng.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
	quadcgrprlng.x	$⊢ φ \to X \in P$
	quadcgrprlng.y	$⊢ φ \to Y \in P$
	quadcgrprlng.z	$⊢ φ \to Z \in P$
	quadcgrprlng.w	$⊢ φ \to W \in P$
	quadcgrprlng.2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
	quadcgrprlng.3	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$
	quadcgrprlng.4	$⊢ φ \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
	quadcgrprlng.5	$⊢ φ \to Y O W$
Assertion	quadcgrprlng	$⊢ φ \to ((Y L Z) \underset{˙}{∥} (W L X) \land Y \underset{˙}{-} Z = W \underset{˙}{-} X)$

Proof

Step	Hyp	Ref	Expression
1		quadcgrprlng.p	$⊢ P = {Base}_{G}$
2		quadcgrprlng.d	$⊢ \underset{˙}{-} = dist (G)$
3		quadcgrprlng.i	$⊢ I = Itv (G)$
4		quadcgrprlng.l	$⊢ L = {Line}_{𝒢} (G)$
5		quadcgrprlng.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
6		quadcgrprlng.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))\}$
7		quadcgrprlng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		quadcgrprlng.1	$⊢ φ \to G \in 𝒢_{Tarski}^{E}$
9		quadcgrprlng.x	$⊢ φ \to X \in P$
10		quadcgrprlng.y	$⊢ φ \to Y \in P$
11		quadcgrprlng.z	$⊢ φ \to Z \in P$
12		quadcgrprlng.w	$⊢ φ \to W \in P$
13		quadcgrprlng.2	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
14		quadcgrprlng.3	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L W)$
15		quadcgrprlng.4	$⊢ φ \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
16		quadcgrprlng.5	$⊢ φ \to Y O W$
17		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for \|- ( PlnG ` G ) = ( PlnG ` G ) with typecode \|-
18	7	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to G \in 𝒢_{Tarski}$
19	8	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to G \in 𝒢_{Tarski}^{E}$
20	1 4 3 7 10 11 9 13	ncolrot2	$⊢ φ \to \neg (Z \in (X L Y) \lor X = Y)$
21	1 3 4 7 11 9 10 20	ncolne2	$⊢ φ \to Z \neq Y$
22	21	necomd	$⊢ φ \to Y \neq Z$
23	1 3 4 7 10 11 22	tgelrnln	$⊢ φ \to Y L Z \in ran L$
24	23	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to Y L Z \in ran L$
25	13	orsild	$⊢ φ \to \neg X \in (Y L Z)$
26	9 25	eldifd	$⊢ φ \to X \in (P ∖ (Y L Z))$
27	26	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to X \in (P ∖ (Y L Z))$
28	1 4 17 18 24 27	tgelrnpln	Could not format ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> ( ( Y L Z ) ( PlnG ` G ) X ) e. ran ( PlnG ` G ) ) : No typesetting found for \|- ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> ( ( Y L Z ) ( PlnG ` G ) X ) e. ran ( PlnG ` G ) ) with typecode \|-
29	4 5 7 14	prlngrcl2	$⊢ φ \to Z L W \in ran L$
30	29	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to Z L W \in ran L$
31	1 3 4 7 10 11 22	tglinerflx2	$⊢ φ \to Z \in (Y L Z)$
32	1 3 4 7 11 12 29	tglnne	$⊢ φ \to Z \neq W$
33	1 3 4 7 11 12 32	tglinerflx1	$⊢ φ \to Z \in (Z L W)$
34	31 33	elind	$⊢ φ \to Z \in ((Y L Z) \cap (Z L W))$
35	34	ne0d	$⊢ φ \to (Y L Z) \cap (Z L W) \neq \emptyset$
36	35	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to (Y L Z) \cap (Z L W) \neq \emptyset$
37	20	orsild	$⊢ φ \to \neg Z \in (X L Y)$
38	31	adantr	$⊢ (φ \land Y L Z = Z L W) \to Z \in (Y L Z)$
39	7	adantr	$⊢ (φ \land Y L Z = Z L W) \to G \in 𝒢_{Tarski}$
40	8	adantr	$⊢ (φ \land Y L Z = Z L W) \to G \in 𝒢_{Tarski}^{E}$
41	4 17 5 7 14	prlngsym	$⊢ φ \to (Z L W) \underset{˙}{∥} (X L Y)$
42	41	adantr	$⊢ (φ \land Y L Z = Z L W) \to (Z L W) \underset{˙}{∥} (X L Y)$
43	29	adantr	$⊢ (φ \land Y L Z = Z L W) \to Z L W \in ran L$
44	4 17 5 39 43	prlngref	$⊢ (φ \land Y L Z = Z L W) \to (Z L W) \underset{˙}{∥} (Z L W)$
45		simpr	$⊢ (φ \land Y L Z = Z L W) \to Y L Z = Z L W$
46	44 45	breqtrrd	$⊢ (φ \land Y L Z = Z L W) \to (Z L W) \underset{˙}{∥} (Y L Z)$
47	1 3 4 7 9 10 11 13	ncolne1	$⊢ φ \to X \neq Y$
48	1 3 4 7 9 10 47	tglinerflx2	$⊢ φ \to Y \in (X L Y)$
49	48	adantr	$⊢ (φ \land Y L Z = Z L W) \to Y \in (X L Y)$
50	1 3 4 7 10 11 22	tglinerflx1	$⊢ φ \to Y \in (Y L Z)$
51	50	adantr	$⊢ (φ \land Y L Z = Z L W) \to Y \in (Y L Z)$
52	1 5 39 40 42 46 49 51	prlngeq	$⊢ (φ \land Y L Z = Z L W) \to X L Y = Y L Z$
53	38 52	eleqtrrd	$⊢ (φ \land Y L Z = Z L W) \to Z \in (X L Y)$
54	37 53	mtand	$⊢ φ \to \neg Y L Z = Z L W$
55	54	neqned	$⊢ φ \to Y L Z \neq Z L W$
56	55	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to Y L Z \neq Z L W$
57		simplr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to (Y L Z) \underset{˙}{∥} a$
58	1 3 4 17 18 24 27	elplnglnid	Could not format ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> ( Y L Z ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> ( Y L Z ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) with typecode \|-
59		simpr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to X \in a$
60	25	ad3antrrr	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to \neg X \in (Y L Z)$
61		nelne1	$⊢ (X \in a \land \neg X \in (Y L Z)) \to a \neq Y L Z$
62	59 60 61	syl2anc	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to a \neq Y L Z$
63	62	necomd	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to Y L Z \neq a$
64	4 17 5 18 57 63 59	prlngpln3	Could not format ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> a C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> a C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) with typecode \|-
65	1 3 4 7 9 10 11 12 13	tglineneq	$⊢ φ \to X L Y \neq Z L W$
66	4 17 5 7 14 65 33	prlngpln3	Could not format ( ph -> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) Z ) ) : No typesetting found for \|- ( ph -> ( Z L W ) C_ ( ( X L Y ) ( PlnG ` G ) Z ) ) with typecode \|-
67	1 4 3 7 10 11 9 13	ncolcom	$⊢ φ \to \neg (X \in (Z L Y) \lor Z = Y)$
68	67	orsild	$⊢ φ \to \neg X \in (Z L Y)$
69	9 68	eldifd	$⊢ φ \to X \in (P ∖ (Z L Y))$
70	11 37	eldifd	$⊢ φ \to Z \in (P ∖ (X L Y))$
71	1 3 4 17 7 69 10 70 47	plngrot	Could not format ( ph -> ( ( X L Y ) ( PlnG ` G ) Z ) = ( ( Z L Y ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ph -> ( ( X L Y ) ( PlnG ` G ) Z ) = ( ( Z L Y ) ( PlnG ` G ) X ) ) with typecode \|-
72	1 3 4 7 11 10 21	tglinecom	$⊢ φ \to Z L Y = Y L Z$
73	72	oveq1d	Could not format ( ph -> ( ( Z L Y ) ( PlnG ` G ) X ) = ( ( Y L Z ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ph -> ( ( Z L Y ) ( PlnG ` G ) X ) = ( ( Y L Z ) ( PlnG ` G ) X ) ) with typecode \|-
74	71 73	eqtr2d	Could not format ( ph -> ( ( Y L Z ) ( PlnG ` G ) X ) = ( ( X L Y ) ( PlnG ` G ) Z ) ) : No typesetting found for \|- ( ph -> ( ( Y L Z ) ( PlnG ` G ) X ) = ( ( X L Y ) ( PlnG ` G ) Z ) ) with typecode \|-
75	66 74	sseqtrrd	Could not format ( ph -> ( Z L W ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ph -> ( Z L W ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) with typecode \|-
76	75	ad3antrrr	Could not format ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> ( Z L W ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) : No typesetting found for \|- ( ( ( ( ph /\ a e. ran L ) /\ ( Y L Z ) .\|\| a ) /\ X e. a ) -> ( Z L W ) C_ ( ( Y L Z ) ( PlnG ` G ) X ) ) with typecode \|-
77	4 17 5 18 19 28 30 36 56 57 58 64 76	prlnginn0	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to a \cap (Z L W) \neq \emptyset$
78		simpllr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to (Y L Z) \underset{˙}{∥} a$
79	18	adantr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to G \in 𝒢_{Tarski}$
80	30	adantr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z L W \in ran L$
81		simpr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \in (a \cap (Z L W))$
82	81	elin2d	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \in (Z L W)$
83	1 4 3 79 80 82	tglnpt	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \in P$
84	9	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to X \in P$
85	33	adantr	$⊢ (φ \land X \in (Z L W)) \to Z \in (Z L W)$
86	7	adantr	$⊢ (φ \land X \in (Z L W)) \to G \in 𝒢_{Tarski}$
87	8	adantr	$⊢ (φ \land X \in (Z L W)) \to G \in 𝒢_{Tarski}^{E}$
88	1 3 4 7 9 10 47	tgelrnln	$⊢ φ \to X L Y \in ran L$
89	88	adantr	$⊢ (φ \land X \in (Z L W)) \to X L Y \in ran L$
90	4 17 5 86 89	prlngref	$⊢ (φ \land X \in (Z L W)) \to (X L Y) \underset{˙}{∥} (X L Y)$
91	14	adantr	$⊢ (φ \land X \in (Z L W)) \to (X L Y) \underset{˙}{∥} (Z L W)$
92	1 3 4 7 9 10 47	tglinerflx1	$⊢ φ \to X \in (X L Y)$
93	92	adantr	$⊢ (φ \land X \in (Z L W)) \to X \in (X L Y)$
94		simpr	$⊢ (φ \land X \in (Z L W)) \to X \in (Z L W)$
95	1 5 86 87 90 91 93 94	prlngeq	$⊢ (φ \land X \in (Z L W)) \to X L Y = Z L W$
96	85 95	eleqtrrd	$⊢ (φ \land X \in (Z L W)) \to Z \in (X L Y)$
97	37 96	mtand	$⊢ φ \to \neg X \in (Z L W)$
98	97	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to \neg X \in (Z L W)$
99		nelne2	$⊢ (w \in (Z L W) \land \neg X \in (Z L W)) \to w \neq X$
100	82 98 99	syl2anc	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \neq X$
101		simp-4r	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to a \in ran L$
102	81	elin1d	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \in a$
103		simplr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to X \in a$
104	1 3 4 79 83 84 100 100 101 102 103	tglinethru	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to a = w L X$
105	78 104	breqtrd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to (Y L Z) \underset{˙}{∥} (w L X)$
106		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
107	11	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z \in P$
108	10	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Y \in P$
109	12	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to W \in P$
110	32	necomd	$⊢ φ \to W \neq Z$
111	110	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to W \neq Z$
112	47	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to X \neq Y$
113	1 3 4 7 9 10 11 13	ncolne2	$⊢ φ \to X \neq Z$
114	1 3 4 7 9 11 113	tgelrnln	$⊢ φ \to X L Z \in ran L$
115	114	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to X L Z \in ran L$
116	1 2 3 6 4 114 7 10 12 16	oppcom	$⊢ φ \to W O Y$
117	116	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to W O Y$
118	1 3 4 7 9 11 113	tglinerflx2	$⊢ φ \to Z \in (X L Z)$
119	118	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z \in (X L Z)$
120	19	adantr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to G \in 𝒢_{Tarski}^{E}$
121	13	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to \neg (X \in (Y L Z) \lor Y = Z)$
122	14	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to (X L Y) \underset{˙}{∥} (Z L W)$
123	25	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to \neg X \in (Y L Z)$
124		simpllr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to X \in a$
125	79	adantr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to G \in 𝒢_{Tarski}$
126	120	adantr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to G \in 𝒢_{Tarski}^{E}$
127	4 17 5 7 23	prlngref	$⊢ φ \to (Y L Z) \underset{˙}{∥} (Y L Z)$
128	127	ad5antr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to (Y L Z) \underset{˙}{∥} (Y L Z)$
129		simp-4r	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to (Y L Z) \underset{˙}{∥} a$
130	31	ad5antr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to Z \in (Y L Z)$
131		simpr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to Z = w$
132	102	adantr	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to w \in a$
133	131 132	eqeltrd	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to Z \in a$
134	1 5 125 126 128 129 130 133	prlngeq	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to Y L Z = a$
135	124 134	eleqtrrd	$⊢ (((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \land Z = w) \to X \in (Y L Z)$
136	123 135	mtand	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to \neg Z = w$
137	136	neqned	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z \neq w$
138	33	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z \in (Z L W)$
139	1 3 4 79 107 83 137 137 80 138 82	tglinethru	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z L W = Z L w$
140	122 139	breqtrd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to (X L Y) \underset{˙}{∥} (Z L w)$
141	1 2 4 5 79 120 84 108 107 83 121 140 105 6 3	prlngsymquadopp	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w O Y$
142	1 3 4 7 11 12 32	tglinecom	$⊢ φ \to Z L W = W L Z$
143	142	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z L W = W L Z$
144	82 143	eleqtrd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \in (W L Z)$
145	1 3 4 6 106 79 115 109 108 117 119 141 144	hlopp	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w {hl}_{𝒢} (G) (Z) W$
146	1 3 106 12 9 11 7 110	hlid	$⊢ φ \to W {hl}_{𝒢} (G) (Z) W$
147	146	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to W {hl}_{𝒢} (G) (Z) W$
148	1 2 4 5 79 120 84 108 107 83 121 140 105	prlngsymquad	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to (X \underset{˙}{-} Y = Z \underset{˙}{-} w \land Y \underset{˙}{-} Z = w \underset{˙}{-} X)$
149	148	simpld	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to X \underset{˙}{-} Y = Z \underset{˙}{-} w$
150	149	eqcomd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z \underset{˙}{-} w = X \underset{˙}{-} Y$
151	15	eqcomd	$⊢ φ \to Z \underset{˙}{-} W = X \underset{˙}{-} Y$
152	151	ad4antr	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Z \underset{˙}{-} W = X \underset{˙}{-} Y$
153	1 2 106 107 84 108 79 109 111 112 145 147 150 152	hlcgreq	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w = W$
154	153	oveq1d	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w L X = W L X$
155	105 154	breqtrd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to (Y L Z) \underset{˙}{∥} (W L X)$
156	148	simprd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Y \underset{˙}{-} Z = w \underset{˙}{-} X$
157	153	oveq1d	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to w \underset{˙}{-} X = W \underset{˙}{-} X$
158	156 157	eqtrd	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to Y \underset{˙}{-} Z = W \underset{˙}{-} X$
159	155 158	jca	$⊢ ((((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \land w \in (a \cap (Z L W))) \to ((Y L Z) \underset{˙}{∥} (W L X) \land Y \underset{˙}{-} Z = W \underset{˙}{-} X)$
160	77 159	n0limd	$⊢ (((φ \land a \in ran L) \land (Y L Z) \underset{˙}{∥} a) \land X \in a) \to ((Y L Z) \underset{˙}{∥} (W L X) \land Y \underset{˙}{-} Z = W \underset{˙}{-} X)$
161	160	anasss	$⊢ ((φ \land a \in ran L) \land ((Y L Z) \underset{˙}{∥} a \land X \in a)) \to ((Y L Z) \underset{˙}{∥} (W L X) \land Y \underset{˙}{-} Z = W \underset{˙}{-} X)$
162	1 4 5 7 23 9	prlngex	$⊢ φ \to \exists a \in ran L ((Y L Z) \underset{˙}{∥} a \land X \in a)$
163	161 162	r19.29a	$⊢ φ \to ((Y L Z) \underset{˙}{∥} (W L X) \land Y \underset{˙}{-} Z = W \underset{˙}{-} X)$

Metamath Proof Explorer

Theorem quadcgrprlng

Proof