prlngsymquadlem

	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)$
	prlngsymquadlem.t	$⊢ T = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y)$
Assertion	prlngsymquadlem	$⊢ φ \to T = W$

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		prlngsymquadlem.t	$⊢ T = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y)$
15		eqid	$⊢ Itv (G) = Itv (G)$
16	3 4 5 13	prlngrcl2	$⊢ φ \to W L X \in ran L$
17	1 15 3 5 10 7 16	tglnne	$⊢ φ \to W \neq X$
18	1 15 3 5 10 7 17	tglinecom	$⊢ φ \to W L X = X L W$
19	18 16	eqeltrrd	$⊢ φ \to X L W \in ran L$
20	3 4 5 12	prlngrcl2	$⊢ φ \to Z L W \in ran L$
21	1 15 3 5 7 8 9 10 11	tglineneq	$⊢ φ \to X L Y \neq Z L W$
22	5	ad2antrr	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to G \in 𝒢_{Tarski}$
23	12	ad2antrr	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to (X L Y) \underset{˙}{∥} (Z L W)$
24		simpr	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to X L Y \neq Z L W$
25	3 4 22 23 24	prlngin0	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to (X L Y) \cap (Z L W) = \emptyset$
26	1 15 3 5 7 8 9 11	ncolne1	$⊢ φ \to X \neq Y$
27	1 15 3 5 7 8 26	tglinerflx1	$⊢ φ \to X \in (X L Y)$
28	27	ad2antrr	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to X \in (X L Y)$
29	17	necomd	$⊢ φ \to X \neq W$
30	1 15 3 5 7 10 29	tglinerflx1	$⊢ φ \to X \in (X L W)$
31	30	ad2antrr	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to X \in (X L W)$
32		simplr	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to X L W = Z L W$
33	31 32	eleqtrd	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to X \in (Z L W)$
34	28 33	elind	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to X \in ((X L Y) \cap (Z L W))$
35	34	ne0d	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to (X L Y) \cap (Z L W) \neq \emptyset$
36	35	neneqd	$⊢ ((φ \land X L W = Z L W) \land X L Y \neq Z L W) \to \neg (X L Y) \cap (Z L W) = \emptyset$
37	25 36	pm2.65da	$⊢ (φ \land X L W = Z L W) \to \neg X L Y \neq Z L W$
38		nne	$⊢ \neg X L Y \neq Z L W \leftrightarrow X L Y = Z L W$
39	37 38	sylib	$⊢ (φ \land X L W = Z L W) \to X L Y = Z L W$
40	21 39	mteqand	$⊢ φ \to X L W \neq Z L W$
41		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
42	1 3 15 5 8 9 7 11	ncoltgdim2	$⊢ φ \to G {Dim}_{𝒢} \geq 2$
43	1 2 15 5 42 7 9	midcl	$⊢ φ \to X {mid}_{𝒢} (G) Z \in P$
44		eqid	$⊢ {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z)$
45	1 2 15 3 41 5 43 44 8	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) \in P$
46	14 45	eqeltrid	$⊢ φ \to T \in P$
47	3 4 5 13	prlngrcl1	$⊢ φ \to Y L Z \in ran L$
48	1 15 3 5 8 9 47	tglnne	$⊢ φ \to Y \neq Z$
49	48	necomd	$⊢ φ \to Z \neq Y$
50	1 41 44 5 43 9 8	mirleqb	$⊢ φ \to (Z = Y \leftrightarrow {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Z) = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y))$
51	50	necon3bid	$⊢ φ \to (Z \neq Y \leftrightarrow {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Z) \neq {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y))$
52	49 51	mpbid	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Z) \neq {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y)$
53		eqidd	$⊢ φ \to X {mid}_{𝒢} (G) Z = X {mid}_{𝒢} (G) Z$
54	1 2 15 5 42 7 9 41 43	ismidb	$⊢ φ \to (Z = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (X) \leftrightarrow X {mid}_{𝒢} (G) Z = X {mid}_{𝒢} (G) Z)$
55	53 54	mpbird	$⊢ φ \to Z = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (X)$
56	55	eqcomd	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (X) = Z$
57	1 2 15 3 41 5 43 44 7 56	mircom	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Z) = X$
58	14	eqcomi	$⊢ {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) = T$
59	58	a1i	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) = T$
60	52 57 59	3netr3d	$⊢ φ \to X \neq T$
61	1 15 3 5 7 46 60	tglinerflx2	$⊢ φ \to T \in (X L T)$
62	1 41 44 5 43 7 8	mirleqb	$⊢ φ \to (X = Y \leftrightarrow {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (X) = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y))$
63	62	necon3bid	$⊢ φ \to (X \neq Y \leftrightarrow {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (X) \neq {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y))$
64	26 63	mpbid	$⊢ φ \to {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (X) \neq {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y)$
65	64 56 59	3netr3d	$⊢ φ \to Z \neq T$
66	1 15 3 5 9 46 65	tglinerflx2	$⊢ φ \to T \in (Z L T)$
67	61 66	elind	$⊢ φ \to T \in ((X L T) \cap (Z L T))$
68	1 15 3 5 8 9 48	tglinecom	$⊢ φ \to Y L Z = Z L Y$
69		eqid	Could not format ( PlnG ` G ) = ( PlnG ` G ) : No typesetting found for \|- ( PlnG ` G ) = ( PlnG ` G ) with typecode \|-
70		eqid	$⊢ {mid}_{𝒢} (G) = {mid}_{𝒢} (G)$
71	1 3 15 5 8 9 7 11	ncolcom	$⊢ φ \to \neg (X \in (Z L Y) \lor Z = Y)$
72	71	orsild	$⊢ φ \to \neg X \in (Z L Y)$
73	7 72	eldifd	$⊢ φ \to X \in (P ∖ (Z L Y))$
74	1 2 15 5 42 9 7	midcom	$⊢ φ \to Z {mid}_{𝒢} (G) X = X {mid}_{𝒢} (G) Z$
75	1 2 15 5 42 8 46 41 43	ismidb	$⊢ φ \to (T = {pInv}_{𝒢} (G) (X {mid}_{𝒢} (G) Z) (Y) \leftrightarrow Y {mid}_{𝒢} (G) T = X {mid}_{𝒢} (G) Z)$
76	14 75	mpbii	$⊢ φ \to Y {mid}_{𝒢} (G) T = X {mid}_{𝒢} (G) Z$
77	76	eqcomd	$⊢ φ \to X {mid}_{𝒢} (G) Z = Y {mid}_{𝒢} (G) T$
78	74 77	eqtrd	$⊢ φ \to Z {mid}_{𝒢} (G) X = Y {mid}_{𝒢} (G) T$
79	1 3 69 4 70 5 6 9 8 73 46 78 49	prlngmid2	$⊢ φ \to (Z L Y) \underset{˙}{∥} (X L T)$
80	68 79	eqbrtrd	$⊢ φ \to (Y L Z) \underset{˙}{∥} (X L T)$
81	13 18	breqtrd	$⊢ φ \to (Y L Z) \underset{˙}{∥} (X L W)$
82	1 15 3 5 7 46 60	tglinerflx1	$⊢ φ \to X \in (X L T)$
83	1 4 5 6 80 81 82 30	prlngeq	$⊢ φ \to X L T = X L W$
84	1 3 15 5 8 9 7 11	ncolrot2	$⊢ φ \to \neg (Z \in (X L Y) \lor X = Y)$
85	84	orsild	$⊢ φ \to \neg Z \in (X L Y)$
86	9 85	eldifd	$⊢ φ \to Z \in (P ∖ (X L Y))$
87	1 3 69 4 70 5 6 7 8 86 46 77 26	prlngmid2	$⊢ φ \to (X L Y) \underset{˙}{∥} (Z L T)$
88	1 15 3 5 9 46 65	tglinerflx1	$⊢ φ \to Z \in (Z L T)$
89	1 15 3 5 9 10 20	tglnne	$⊢ φ \to Z \neq W$
90	1 15 3 5 9 10 89	tglinerflx1	$⊢ φ \to Z \in (Z L W)$
91	1 4 5 6 87 12 88 90	prlngeq	$⊢ φ \to Z L T = Z L W$
92	83 91	ineq12d	$⊢ φ \to (X L T) \cap (Z L T) = (X L W) \cap (Z L W)$
93	67 92	eleqtrd	$⊢ φ \to T \in ((X L W) \cap (Z L W))$
94	1 15 3 5 7 10 29	tglinerflx2	$⊢ φ \to W \in (X L W)$
95	1 15 3 5 9 10 89	tglinerflx2	$⊢ φ \to W \in (Z L W)$
96	94 95	elind	$⊢ φ \to W \in ((X L W) \cap (Z L W))$
97	1 15 3 5 19 20 40 93 96	tglineineq	$⊢ φ \to T = W$

Metamath Proof Explorer

Theorem prlngsymquadlem

Proof