lnssplnglem

	Ref	Expression
Hypotheses	plngval.p	$⊢ P = {Base}_{G}$
	plngval.i	$⊢ I = Itv (G)$
	plngval.1	$⊢ L = {Line}_{𝒢} (G)$
	plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	lnssplnglem.x	$⊢ φ \to X \in (A E R)$
	lnssplnglem.y	$⊢ φ \to Y \in (A E R)$
	lnssplnglem.1	$⊢ φ \to X \neq Y$
	lnssplnglem.2	$⊢ φ \to A \in ran L$
	lnssplnglem.3	$⊢ φ \to R \in (P ∖ A)$
	lnssplnglem.4	$⊢ φ \to A \neq X L Y$
	lnssplnglem.5	$⊢ φ \to \neg Y \in A$
Assertion	lnssplnglem	$⊢ φ \to (X L Y \subseteq A E R \land \exists s \in (P ∖ (X L Y)) A E R = (X L Y) E s)$

Proof

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		lnssplnglem.x	$⊢ φ \to X \in (A E R)$
7		lnssplnglem.y	$⊢ φ \to Y \in (A E R)$
8		lnssplnglem.1	$⊢ φ \to X \neq Y$
9		lnssplnglem.2	$⊢ φ \to A \in ran L$
10		lnssplnglem.3	$⊢ φ \to R \in (P ∖ A)$
11		lnssplnglem.4	$⊢ φ \to A \neq X L Y$
12		lnssplnglem.5	$⊢ φ \to \neg Y \in A$
13	5	adantr	$⊢ (φ \land z \in A) \to G \in 𝒢_{Tarski}$
14	13	adantr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to G \in 𝒢_{Tarski}$
15	1 2 3 4 5 9 10 6	plngssp	$⊢ φ \to X \in P$
16	15	adantr	$⊢ (φ \land z \in A) \to X \in P$
17	1 2 3 4 5 9 10 7	plngssp	$⊢ φ \to Y \in P$
18	17	adantr	$⊢ (φ \land z \in A) \to Y \in P$
19	8	adantr	$⊢ (φ \land z \in A) \to X \neq Y$
20	1 2 3 13 16 18 19	tgelrnln	$⊢ (φ \land z \in A) \to X L Y \in ran L$
21	20	adantr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to X L Y \in ran L$
22	9	ad2antrr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to A \in ran L$
23		simplr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to z \in A$
24	1 3 2 14 22 23	tglnpt	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to z \in P$
25		simpr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to \neg z \in (X L Y)$
26	24 25	eldifd	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to z \in (P ∖ (X L Y))$
27	1 2 3 4 14 21 26	elplnglnid	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to X L Y \subseteq (X L Y) E z$
28	16	adantr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to X \in P$
29	14	adantr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to G \in 𝒢_{Tarski}$
30	28	adantr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to X \in P$
31	18	ad2antrr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to Y \in P$
32	24	adantr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to z \in P$
33	19	ad2antrr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to X \neq Y$
34	1 2 3 5 15 17 8	tglinerflx2	$⊢ φ \to Y \in (X L Y)$
35	34	ad3antrrr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to Y \in (X L Y)$
36		simplr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to \neg z \in (X L Y)$
37		nelne2	$⊢ (Y \in (X L Y) \land \neg z \in (X L Y)) \to Y \neq z$
38	35 36 37	syl2anc	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to Y \neq z$
39		simpr	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to X \in (z L Y)$
40	1 2 3 29 31 32 30 38 39	lncom	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to X \in (Y L z)$
41	1 2 3 29 30 31 32 33 40 38	lnrot2	$⊢ (((φ \land z \in A) \land \neg z \in (X L Y)) \land X \in (z L Y)) \to z \in (X L Y)$
42	25 41	mtand	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to \neg X \in (z L Y)$
43	28 42	eldifd	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to X \in (P ∖ (z L Y))$
44	18	adantr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to Y \in P$
45	19	adantr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to X \neq Y$
46	1 2 3 4 14 43 44 26 45	plngrot	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to (X L Y) E z = (z L Y) E X$
47	46	ad2antrr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to (X L Y) E z = (z L Y) E X$
48	5	ad4antr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to G \in 𝒢_{Tarski}$
49	24	ad2antrr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to z \in P$
50	17	ad4antr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to Y \in P$
51	23	ad2antrr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to z \in A$
52	12	ad4antr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to \neg Y \in A$
53		nelne2	$⊢ (z \in A \land \neg Y \in A) \to z \neq Y$
54	51 52 53	syl2anc	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to z \neq Y$
55	1 2 3 48 49 50 54	tgelrnln	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to z L Y \in ran L$
56	9	ad4antr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to A \in ran L$
57		simplr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to w \in (A ∖ (Y L z))$
58	57	eldifad	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to w \in A$
59	1 3 2 48 56 58	tglnpt	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to w \in P$
60	57	eldifbd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to \neg w \in (Y L z)$
61	1 2 3 48 49 50 54	tglinecom	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to z L Y = Y L z$
62	60 61	neleqtrrd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to \neg w \in (z L Y)$
63	59 62	eldifd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to w \in (P ∖ (z L Y))$
64	6	ad4antr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to X \in (A E R)$
65		simpr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to w \neq z$
66	1 2 3 48 59 49 65 65 56 58 51	tglinethru	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to A = w L z$
67	52 66	neleqtrd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to \neg Y \in (w L z)$
68	50 67	eldifd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to Y \in (P ∖ (w L z))$
69	59 60	eldifd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to w \in (P ∖ (Y L z))$
70	54	necomd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to Y \neq z$
71	1 2 3 4 48 68 49 69 70	plngrot	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to (Y L z) E w = (w L z) E Y$
72	61	oveq1d	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to (z L Y) E w = (Y L z) E w$
73	66	oveq1d	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to A E Y = (w L z) E Y$
74	71 72 73	3eqtr4d	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to (z L Y) E w = A E Y$
75	7 12	eldifd	$⊢ φ \to Y \in ((A E R) ∖ A)$
76	1 2 3 4 5 9 10 75	plngcp	$⊢ φ \to A E R = A E Y$
77	76	ad4antr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to A E R = A E Y$
78	74 77	eqtr4d	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to (z L Y) E w = A E R$
79	64 78	eleqtrrd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to X \in ((z L Y) E w)$
80	42	ad2antrr	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to \neg X \in (z L Y)$
81	79 80	eldifd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to X \in (((z L Y) E w) ∖ (z L Y))$
82	1 2 3 4 48 55 63 81	plngcp	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to (z L Y) E w = (z L Y) E X$
83	47 82 78	3eqtr2rd	$⊢ ((((φ \land z \in A) \land \neg z \in (X L Y)) \land w \in (A ∖ (Y L z))) \land w \neq z) \to A E R = (X L Y) E z$
84	34	ad2antrr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to Y \in (X L Y)$
85	84 25 37	syl2anc	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to Y \neq z$
86	1 2 3 14 44 24 85	tgelrnln	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to Y L z \in ran L$
87	1 2 3 14 44 24 85	tglinerflx1	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to Y \in (Y L z)$
88	12	ad2antrr	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to \neg Y \in A$
89		nelne1	$⊢ (Y \in (Y L z) \land \neg Y \in A) \to Y L z \neq A$
90	87 88 89	syl2anc	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to Y L z \neq A$
91	90	necomd	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to A \neq Y L z$
92	1 2 3 14 22 86 23 91	tglnpt4	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to \exists w \in (A ∖ (Y L z)) w \neq z$
93	83 92	r19.29a	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to A E R = (X L Y) E z$
94	27 93	sseqtrrd	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to X L Y \subseteq A E R$
95		oveq2	$⊢ s = z \to (X L Y) E s = (X L Y) E z$
96	95	eqeq2d	$⊢ s = z \to (A E R = (X L Y) E s \leftrightarrow A E R = (X L Y) E z)$
97	96 26 93	rspcedvdw	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to \exists s \in (P ∖ (X L Y)) A E R = (X L Y) E s$
98	94 97	jca	$⊢ ((φ \land z \in A) \land \neg z \in (X L Y)) \to (X L Y \subseteq A E R \land \exists s \in (P ∖ (X L Y)) A E R = (X L Y) E s)$
99	11	neneqd	$⊢ φ \to \neg A = X L Y$
100	5	adantr	$⊢ (φ \land A \subseteq X L Y) \to G \in 𝒢_{Tarski}$
101	9	adantr	$⊢ (φ \land A \subseteq X L Y) \to A \in ran L$
102	15	adantr	$⊢ (φ \land A \subseteq X L Y) \to X \in P$
103	17	adantr	$⊢ (φ \land A \subseteq X L Y) \to Y \in P$
104	8	adantr	$⊢ (φ \land A \subseteq X L Y) \to X \neq Y$
105	1 2 3 100 102 103 104	tgelrnln	$⊢ (φ \land A \subseteq X L Y) \to X L Y \in ran L$
106		simpr	$⊢ (φ \land A \subseteq X L Y) \to A \subseteq X L Y$
107	3 100 101 105 106	tglinesseq	$⊢ (φ \land A \subseteq X L Y) \to A = X L Y$
108	99 107	mtand	$⊢ φ \to \neg A \subseteq X L Y$
109		nssrex	$⊢ \neg A \subseteq X L Y \leftrightarrow \exists z \in A \neg z \in (X L Y)$
110	108 109	sylib	$⊢ φ \to \exists z \in A \neg z \in (X L Y)$
111	98 110	r19.29a	$⊢ φ \to (X L Y \subseteq A E R \land \exists s \in (P ∖ (X L Y)) A E R = (X L Y) E s)$

Metamath Proof Explorer

Theorem lnssplnglem

Proof