lnincplng

Description: If two lines A and B intersect, then B is in a plane defined by A and any point of B . Lemma 9.22 of Schwabhauser p. 74. (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}$
	lnincplng.a	$⊢ φ \to A \in ran L$
	lnincplng.b	$⊢ φ \to B \in ran L$
	lnincplng.x	$⊢ φ \to X \in B$
	lnincplng.y	$⊢ φ \to Y \in P$
	lnincplng.1	$⊢ φ \to X \neq Y$
	lnincplng.2	$⊢ φ \to A \cap B = \{Y\}$
Assertion	lnincplng	$⊢ φ \to B \subseteq A E X$

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		lnincplng.a	$⊢ φ \to A \in ran L$
7		lnincplng.b	$⊢ φ \to B \in ran L$
8		lnincplng.x	$⊢ φ \to X \in B$
9		lnincplng.y	$⊢ φ \to Y \in P$
10		lnincplng.1	$⊢ φ \to X \neq Y$
11		lnincplng.2	$⊢ φ \to A \cap B = \{Y\}$
12		simpr	$⊢ ((φ \land z \in B) \land z = X) \to z = X$
13	1 3 2 5 7 8	tglnpt	$⊢ φ \to X \in P$
14	10	neneqd	$⊢ φ \to \neg X = Y$
15		simpr	$⊢ (φ \land X \in A) \to X \in A$
16	8	adantr	$⊢ (φ \land X \in A) \to X \in B$
17	15 16	elind	$⊢ (φ \land X \in A) \to X \in (A \cap B)$
18	11	adantr	$⊢ (φ \land X \in A) \to A \cap B = \{Y\}$
19	17 18	eleqtrd	$⊢ (φ \land X \in A) \to X \in \{Y\}$
20	19	elsnd	$⊢ (φ \land X \in A) \to X = Y$
21	14 20	mtand	$⊢ φ \to \neg X \in A$
22	13 21	eldifd	$⊢ φ \to X \in (P ∖ A)$
23	1 2 3 4 5 6 22	elplngid	$⊢ φ \to X \in (A E X)$
24	23	ad2antrr	$⊢ ((φ \land z \in B) \land z = X) \to X \in (A E X)$
25	12 24	eqeltrd	$⊢ ((φ \land z \in B) \land z = X) \to z \in (A E X)$
26		simpr	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to z = Y$
27	5	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to G \in 𝒢_{Tarski}$
28	6	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to A \in ran L$
29	22	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to X \in (P ∖ A)$
30	1 2 3 4 27 28 29	elplnglnid	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to A \subseteq A E X$
31		snidg	$⊢ Y \in P \to Y \in \{Y\}$
32	9 31	syl	$⊢ φ \to Y \in \{Y\}$
33	32 11	eleqtrrd	$⊢ φ \to Y \in (A \cap B)$
34	33	elin1d	$⊢ φ \to Y \in A$
35	34	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to Y \in A$
36	30 35	sseldd	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to Y \in (A E X)$
37	26 36	eqeltrd	$⊢ (((φ \land z \in B) \land z \neq X) \land z = Y) \to z \in (A E X)$
38		simpr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to z \neq Y$
39	38	neneqd	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to \neg z = Y$
40		simpr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z \in A) \to z \in A$
41		simpllr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to z \in B$
42	41	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z \in A) \to z \in B$
43	40 42	elind	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z \in A) \to z \in (A \cap B)$
44	11	ad4antr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z \in A) \to A \cap B = \{Y\}$
45	43 44	eleqtrd	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z \in A) \to z \in \{Y\}$
46	45	elsnd	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z \in A) \to z = Y$
47	39 46	mtand	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to \neg z \in A$
48	5	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to G \in 𝒢_{Tarski}$
49	6	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to A \in ran L$
50	7	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to B \in ran L$
51	1 3 2 48 50 41	tglnpt	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to z \in P$
52		eleq1w	$⊢ a = c \to (a \in (P ∖ A) \leftrightarrow c \in (P ∖ A))$
53		eleq1w	$⊢ b = d \to (b \in (P ∖ A) \leftrightarrow d \in (P ∖ A))$
54	52 53	bi2anan9	$⊢ (a = c \land b = d) \to ((a \in (P ∖ A) \land b \in (P ∖ A)) \leftrightarrow (c \in (P ∖ A) \land d \in (P ∖ A)))$
55		eleq1w	$⊢ t = s \to (t \in (a I b) \leftrightarrow s \in (a I b))$
56	55	cbvrexvw	$⊢ \exists t \in A t \in (a I b) \leftrightarrow \exists s \in A s \in (a I b)$
57		oveq12	$⊢ (a = c \land b = d) \to a I b = c I d$
58	57	eleq2d	$⊢ (a = c \land b = d) \to (s \in (a I b) \leftrightarrow s \in (c I d))$
59	58	rexbidv	$⊢ (a = c \land b = d) \to (\exists s \in A s \in (a I b) \leftrightarrow \exists s \in A s \in (c I d))$
60	56 59	bitrid	$⊢ (a = c \land b = d) \to (\exists t \in A t \in (a I b) \leftrightarrow \exists s \in A s \in (c I d))$
61	54 60	anbi12d	$⊢ (a = c \land b = d) \to (((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b)) \leftrightarrow ((c \in (P ∖ A) \land d \in (P ∖ A)) \land \exists s \in A s \in (c I d)))$
62	61	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} = \{⟨c, d⟩ \| ((c \in (P ∖ A) \land d \in (P ∖ A)) \land \exists s \in A s \in (c I d))\}$
63	13	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to X \in P$
64	34	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to Y \in A$
65	9	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to Y \in P$
66		simplr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to z \neq X$
67	33	elin2d	$⊢ φ \to Y \in B$
68	67	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to Y \in B$
69	66	necomd	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to X \neq z$
70	8	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to X \in B$
71	1 2 3 48 63 51 69 69 50 70 41	tglinethru	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to B = X L z$
72	68 71	eleqtrd	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to Y \in (X L z)$
73	1 2 3 48 51 63 65 66 72	lncom	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to Y \in (z L X)$
74	73	orcd	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (Y \in (z L X) \lor z = X)$
75		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
76	1 2 3 48 49 51 62 63 64 74 75	colhp	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z {hp}_{𝒢} (G) (A) X \leftrightarrow (z {hl}_{𝒢} (G) (Y) X \land \neg z \in A))$
77	47 76	mpbiran2d	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z {hp}_{𝒢} (G) (A) X \leftrightarrow z {hl}_{𝒢} (G) (Y) X)$
78	77	biimpar	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land z {hl}_{𝒢} (G) (Y) X) \to z {hp}_{𝒢} (G) (A) X$
79		eqid	$⊢ dist (G) = dist (G)$
80	51	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to z \in P$
81	63	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to X \in P$
82	64	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to Y \in A$
83	47	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to \neg z \in A$
84	21	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to \neg X \in A$
85	84	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to \neg X \in A$
86	48	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to G \in 𝒢_{Tarski}$
87	65	adantr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to Y \in P$
88		simpr	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to Y \in (X I z)$
89	1 79 2 86 81 87 80 88	tgbtwncom	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to Y \in (z I X)$
90	1 79 2 62 80 81 82 83 85 89	islnoppd	$⊢ ((((φ \land z \in B) \land z \neq X) \land z \neq Y) \land Y \in (X I z)) \to z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X$
91	1 2 3 5 13 9 10 10 7 8 67	tglinethru	$⊢ φ \to B = X L Y$
92	91	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to B = X L Y$
93	41 92	eleqtrd	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to z \in (X L Y)$
94	1 2 75 63 65 51 48 63 3 93	lnhl	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z {hl}_{𝒢} (G) (Y) X \lor Y \in (X I z))$
95	78 90 94	orim12da	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z {hp}_{𝒢} (G) (A) X \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X)$
96	95	olcd	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z \in A \lor (z {hp}_{𝒢} (G) (A) X \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X))$
97		3orass	$⊢ (z \in A \lor z {hp}_{𝒢} (G) (A) X \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X) \leftrightarrow (z \in A \lor (z {hp}_{𝒢} (G) (A) X \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X))$
98	96 97	sylibr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z \in A \lor z {hp}_{𝒢} (G) (A) X \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X)$
99	22	ad3antrrr	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to X \in (P ∖ A)$
100	1 2 3 4 48 49 99 62 51	elplng	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to (z \in (A E X) \leftrightarrow (z \in A \lor z {hp}_{𝒢} (G) (A) X \lor z \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\} X))$
101	98 100	mpbird	$⊢ (((φ \land z \in B) \land z \neq X) \land z \neq Y) \to z \in (A E X)$
102	37 101	pm2.61dane	$⊢ ((φ \land z \in B) \land z \neq X) \to z \in (A E X)$
103	25 102	pm2.61dane	$⊢ (φ \land z \in B) \to z \in (A E X)$
104	103	ex	$⊢ φ \to (z \in B \to z \in (A E X))$
105	104	ssrdv	$⊢ φ \to B \subseteq A E X$

Metamath Proof Explorer

Theorem lnincplng

Proof