symquadprlnglem

	Ref	Expression
Hypotheses	symquadprlnglem.p	$⊢ P = {Base}_{G}$
	symquadprlnglem.d	$⊢ \underset{˙}{-} = dist (G)$
	symquadprlnglem.l	$⊢ L = {Line}_{𝒢} (G)$
	symquadprlnglem.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	symquadprlnglem.x	$⊢ φ \to X \in P$
	symquadprlnglem.y	$⊢ φ \to Y \in P$
	symquadprlnglem.z	$⊢ φ \to Z \in P$
	symquadprlnglem.w	$⊢ φ \to W \in P$
	symquadprlnglem.1	$⊢ φ \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
	symquadprlnglem.2	$⊢ φ \to Y \underset{˙}{-} Z = W \underset{˙}{-} X$
	symquadprlnglem.3	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
	symquadprlnglem.4	$⊢ φ \to Y \neq W$
	symquadprlnglem.5	$⊢ φ \to T \in (X L Z)$
	symquadprlnglem.6	$⊢ φ \to T \in (Y L W)$
Assertion	symquadprlnglem	$⊢ φ \to \neg (W \in (Z L Y) \lor Z = Y)$

Proof

Step	Hyp	Ref	Expression
1		symquadprlnglem.p	$⊢ P = {Base}_{G}$
2		symquadprlnglem.d	$⊢ \underset{˙}{-} = dist (G)$
3		symquadprlnglem.l	$⊢ L = {Line}_{𝒢} (G)$
4		symquadprlnglem.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		symquadprlnglem.x	$⊢ φ \to X \in P$
6		symquadprlnglem.y	$⊢ φ \to Y \in P$
7		symquadprlnglem.z	$⊢ φ \to Z \in P$
8		symquadprlnglem.w	$⊢ φ \to W \in P$
9		symquadprlnglem.1	$⊢ φ \to X \underset{˙}{-} Y = Z \underset{˙}{-} W$
10		symquadprlnglem.2	$⊢ φ \to Y \underset{˙}{-} Z = W \underset{˙}{-} X$
11		symquadprlnglem.3	$⊢ φ \to \neg (X \in (Y L Z) \lor Y = Z)$
12		symquadprlnglem.4	$⊢ φ \to Y \neq W$
13		symquadprlnglem.5	$⊢ φ \to T \in (X L Z)$
14		symquadprlnglem.6	$⊢ φ \to T \in (Y L W)$
15		eqid	$⊢ Itv (G) = Itv (G)$
16	1 3 15 4 5 7 13	tglngne	$⊢ φ \to X \neq Z$
17	16	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to X \neq Z$
18	4	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to G \in 𝒢_{Tarski}$
19	1 15 3 4 6 8 12	tgelrnln	$⊢ φ \to Y L W \in ran L$
20	1 3 15 4 19 14	tglnpt	$⊢ φ \to T \in P$
21	20	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to T \in P$
22	7	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to Z \in P$
23	5	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to X \in P$
24		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
25		eqid	$⊢ {pInv}_{𝒢} (G) (T) = {pInv}_{𝒢} (G) (T)$
26	13	orcd	$⊢ φ \to (T \in (X L Z) \lor X = Z)$
27	14	orcd	$⊢ φ \to (T \in (Y L W) \lor Y = W)$
28	1 2 15 3 24 4 25 5 6 7 8 20 11 12 9 10 26 27	symquadlem	$⊢ φ \to X = {pInv}_{𝒢} (G) (T) (Z)$
29	28	oveq2d	$⊢ φ \to T \underset{˙}{-} X = T \underset{˙}{-} {pInv}_{𝒢} (G) (T) (Z)$
30	1 2 15 3 24 4 20 25 7	mircgr	$⊢ φ \to T \underset{˙}{-} {pInv}_{𝒢} (G) (T) (Z) = T \underset{˙}{-} Z$
31	29 30	eqtr2d	$⊢ φ \to T \underset{˙}{-} Z = T \underset{˙}{-} X$
32	31	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to T \underset{˙}{-} Z = T \underset{˙}{-} X$
33		simpr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to T = Z$
34	1 2 15 18 21 22 21 23 32 33	tgcgreq	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to T = X$
35	34 33	eqtr3d	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to X = Z$
36		nne	$⊢ \neg X \neq Z \leftrightarrow X = Z$
37	35 36	sylibr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T = Z) \to \neg X \neq Z$
38	17 37	pm2.65da	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to \neg T = Z$
39	38	neqned	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to T \neq Z$
40	4	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to G \in 𝒢_{Tarski}$
41	7	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to Z \in P$
42	5	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to X \in P$
43	6	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to Y \in P$
44	20	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to T \in P$
45	4	adantr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to G \in 𝒢_{Tarski}$
46	7	adantr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to Z \in P$
47	6	adantr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to Y \in P$
48	20	adantr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to T \in P$
49	8	adantr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to W \in P$
50	1 15 3 4 6 8 12	tglinecom	$⊢ φ \to Y L W = W L Y$
51	14 50	eleqtrd	$⊢ φ \to T \in (W L Y)$
52	51	adantr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to T \in (W L Y)$
53		simpr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to (W \in (Z L Y) \lor Z = Y)$
54	1 3 15 45 46 47 49 53	colcom	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to (W \in (Y L Z) \lor Y = Z)$
55	1 15 3 45 48 49 47 46 52 54	coltr	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to (T \in (Y L Z) \lor Y = Z)$
56	1 3 15 45 47 46 48 55	colcom	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to (T \in (Z L Y) \lor Z = Y)$
57	1 3 15 45 46 47 48 56	colrot2	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to (Y \in (T L Z) \lor T = Z)$
58	57	adantr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to (Y \in (T L Z) \lor T = Z)$
59		simpr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to T \neq Z$
60	59	neneqd	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to \neg T = Z$
61	58 60	olcnd	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to Y \in (T L Z)$
62	1 3 15 4 5 7 20 26	colcom	$⊢ φ \to (T \in (Z L X) \lor Z = X)$
63	62	ad2antrr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to (T \in (Z L X) \lor Z = X)$
64	1 15 3 40 43 44 41 42 61 63	coltr	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to (Y \in (Z L X) \lor Z = X)$
65	1 3 15 40 41 42 43 64	colrot2	$⊢ ((φ \land (W \in (Z L Y) \lor Z = Y)) \land T \neq Z) \to (X \in (Y L Z) \lor Y = Z)$
66	39 65	mpdan	$⊢ (φ \land (W \in (Z L Y) \lor Z = Y)) \to (X \in (Y L Z) \lor Y = Z)$
67	11 66	mtand	$⊢ φ \to \neg (W \in (Z L Y) \lor Z = Y)$

Metamath Proof Explorer

Theorem symquadprlnglem

Proof