lnssplng

Description: A line defined by two points X and Y , both on a plane H , is entirely contained in H . Theorem 9.25 of Schwabhauser p. 75. (Contributed by Thierry Arnoux, 17-Jun-2026)

	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}$
	lnssplng.h	$⊢ φ \to H \in ran E$
	lnssplng.x	$⊢ φ \to X \in H$
	lnssplng.y	$⊢ φ \to Y \in H$
	lnssplng.1	$⊢ φ \to X \neq Y$
Assertion	lnssplng	$⊢ φ \to (X L Y \subseteq H \land \exists s \in (P ∖ (X L Y)) H = (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		lnssplng.h	$⊢ φ \to H \in ran E$
7		lnssplng.x	$⊢ φ \to X \in H$
8		lnssplng.y	$⊢ φ \to Y \in H$
9		lnssplng.1	$⊢ φ \to X \neq Y$
10		simpr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to a = X L Y$
11	5	ad4antr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to G \in 𝒢_{Tarski}$
12		simp-4r	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to a \in ran L$
13		simpllr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to r \in (P ∖ a)$
14	1 2 3 4 11 12 13	elplnglnid	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to a \subseteq a E r$
15	10 14	eqsstrrd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to X L Y \subseteq a E r$
16		oveq2	$⊢ s = r \to (X L Y) E s = (X L Y) E r$
17	16	eqeq2d	$⊢ s = r \to (a E r = (X L Y) E s \leftrightarrow a E r = (X L Y) E r)$
18	13	eldifad	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to r \in P$
19	13	eldifbd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to \neg r \in a$
20	19 10	neleqtrd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to \neg r \in (X L Y)$
21	18 20	eldifd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to r \in (P ∖ (X L Y))$
22	10	oveq1d	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to a E r = (X L Y) E r$
23	17 21 22	rspcedvdw	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = X L Y) \to \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s$
24	15 23	jca	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a = 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)$
25	5	ad4antr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to G \in 𝒢_{Tarski}$
26	25	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to G \in 𝒢_{Tarski}$
27	8	ad4antr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to Y \in H$
28		simplr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to H = a E r$
29	27 28	eleqtrd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to Y \in (a E r)$
30	29	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to Y \in (a E r)$
31	7	ad4antr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to X \in H$
32	31 28	eleqtrd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to X \in (a E r)$
33	32	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to X \in (a E r)$
34	9	necomd	$⊢ φ \to Y \neq X$
35	34	ad5antr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to Y \neq X$
36		simp-4r	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to a \in ran L$
37	36	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to a \in ran L$
38		simpllr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to r \in (P ∖ a)$
39	38	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to r \in (P ∖ a)$
40		simplr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to a \neq X L Y$
41	1 2 3 4 5 6 7	plngrnssp	$⊢ φ \to X \in P$
42	1 2 3 4 5 6 8	plngrnssp	$⊢ φ \to Y \in P$
43	1 2 3 5 41 42 9	tglinecom	$⊢ φ \to X L Y = Y L X$
44	43	ad5antr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to X L Y = Y L X$
45	40 44	neeqtrd	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to a \neq Y L X$
46		simpr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to \neg X \in a$
47	1 2 3 4 26 30 33 35 37 39 45 46	lnssplnglem	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to (Y L X \subseteq a E r \land \exists s \in (P ∖ (Y L X)) a E r = (Y L X) E s)$
48	43	sseq1d	$⊢ φ \to (X L Y \subseteq a E r \leftrightarrow Y L X \subseteq a E r)$
49	43	difeq2d	$⊢ φ \to P ∖ (X L Y) = P ∖ (Y L X)$
50	43	oveq1d	$⊢ φ \to (X L Y) E s = (Y L X) E s$
51	50	eqeq2d	$⊢ φ \to (a E r = (X L Y) E s \leftrightarrow a E r = (Y L X) E s)$
52	49 51	rexeqbidv	$⊢ φ \to (\exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s \leftrightarrow \exists s \in (P ∖ (Y L X)) a E r = (Y L X) E s)$
53	48 52	anbi12d	$⊢ φ \to ((X L Y \subseteq a E r \land \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s) \leftrightarrow (Y L X \subseteq a E r \land \exists s \in (P ∖ (Y L X)) a E r = (Y L X) E s))$
54	53	ad5antr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to ((X L Y \subseteq a E r \land \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s) \leftrightarrow (Y L X \subseteq a E r \land \exists s \in (P ∖ (Y L X)) a E r = (Y L X) E s))$
55	47 54	mpbird	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg X \in a) \to (X L Y \subseteq a E r \land \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s)$
56	25	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to G \in 𝒢_{Tarski}$
57	32	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to X \in (a E r)$
58	29	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to Y \in (a E r)$
59	9	ad4antr	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to X \neq Y$
60	59	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to X \neq Y$
61	36	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to a \in ran L$
62	38	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to r \in (P ∖ a)$
63		simplr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to a \neq X L Y$
64		simpr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to \neg Y \in a$
65	1 2 3 4 56 57 58 60 61 62 63 64	lnssplnglem	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land \neg Y \in a) \to (X L Y \subseteq a E r \land \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s)$
66	59	neneqd	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to \neg X = Y$
67	25	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to G \in 𝒢_{Tarski}$
68	36	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to a \in ran L$
69	1 2 3 4 25 36 38 32	plngssp	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to X \in P$
70	1 2 3 4 25 36 38 29	plngssp	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to Y \in P$
71	1 2 3 25 69 70 59	tgelrnln	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to X L Y \in ran L$
72	71	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X L Y \in ran L$
73		simplr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to a \neq X L Y$
74		simprl	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X \in a$
75	69	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X \in P$
76	70	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to Y \in P$
77	59	adantr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X \neq Y$
78	1 2 3 67 75 76 77	tglinerflx1	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X \in (X L Y)$
79	74 78	elind	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X \in (a \cap (X L Y))$
80		simprr	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to Y \in a$
81	1 2 3 67 75 76 77	tglinerflx2	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to Y \in (X L Y)$
82	80 81	elind	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to Y \in (a \cap (X L Y))$
83	1 2 3 67 68 72 73 79 82	tglineineq	$⊢ (((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \land (X \in a \land Y \in a)) \to X = Y$
84	66 83	mtand	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to \neg (X \in a \land Y \in a)$
85		ianor	$⊢ \neg (X \in a \land Y \in a) \leftrightarrow (\neg X \in a \lor \neg Y \in a)$
86	84 85	sylib	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq X L Y) \to (\neg X \in a \lor \neg Y \in a)$
87	55 65 86	mpjaodan	$⊢ ((((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \land a \neq 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)$
88	24 87	pm2.61dane	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to (X L Y \subseteq a E r \land \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s)$
89		simpr	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to H = a E r$
90	89	sseq2d	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to (X L Y \subseteq H \leftrightarrow X L Y \subseteq a E r)$
91	89	eqeq1d	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to (H = (X L Y) E s \leftrightarrow a E r = (X L Y) E s)$
92	91	rexbidv	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to (\exists s \in (P ∖ (X L Y)) H = (X L Y) E s \leftrightarrow \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s)$
93	90 92	anbi12d	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to ((X L Y \subseteq H \land \exists s \in (P ∖ (X L Y)) H = (X L Y) E s) \leftrightarrow (X L Y \subseteq a E r \land \exists s \in (P ∖ (X L Y)) a E r = (X L Y) E s))$
94	88 93	mpbird	$⊢ (((φ \land a \in ran L) \land r \in (P ∖ a)) \land H = a E r) \to (X L Y \subseteq H \land \exists s \in (P ∖ (X L Y)) H = (X L Y) E s)$
95	1 2 3 4 5 6	isplng	$⊢ φ \to \exists a \in ran L \exists r \in (P ∖ a) H = a E r$
96	94 95	r19.29vva	$⊢ φ \to (X L Y \subseteq H \land \exists s \in (P ∖ (X L Y)) H = (X L Y) E s)$

Metamath Proof Explorer

Theorem lnssplng

Proof