lshpinN

Description: The intersection of two different hyperplanes is not a hyperplane. (Contributed by NM, 29-Oct-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	lshpin.h	$⊢ H = LSHyp (W)$
	lshpin.w	$⊢ φ \to W \in LVec$
	lshpin.t	$⊢ φ \to T \in H$
	lshpin.u	$⊢ φ \to U \in H$
Assertion	lshpinN	$⊢ φ \to (T \cap U \in H \leftrightarrow T = U)$

Step	Hyp	Ref	Expression
1		lshpin.h	$⊢ H = LSHyp (W)$
2		lshpin.w	$⊢ φ \to W \in LVec$
3		lshpin.t	$⊢ φ \to T \in H$
4		lshpin.u	$⊢ φ \to U \in H$
5		inss1	$⊢ T \cap U \subseteq T$
6	2	adantr	$⊢ (φ \land T \cap U \in H) \to W \in LVec$
7		simpr	$⊢ (φ \land T \cap U \in H) \to T \cap U \in H$
8	3	adantr	$⊢ (φ \land T \cap U \in H) \to T \in H$
9	1 6 7 8	lshpcmp	$⊢ (φ \land T \cap U \in H) \to (T \cap U \subseteq T \leftrightarrow T \cap U = T)$
10	5 9	mpbii	$⊢ (φ \land T \cap U \in H) \to T \cap U = T$
11		inss2	$⊢ T \cap U \subseteq U$
12	4	adantr	$⊢ (φ \land T \cap U \in H) \to U \in H$
13	1 6 7 12	lshpcmp	$⊢ (φ \land T \cap U \in H) \to (T \cap U \subseteq U \leftrightarrow T \cap U = U)$
14	11 13	mpbii	$⊢ (φ \land T \cap U \in H) \to T \cap U = U$
15	10 14	eqtr3d	$⊢ (φ \land T \cap U \in H) \to T = U$
16	15	ex	$⊢ φ \to (T \cap U \in H \to T = U)$
17		inidm	$⊢ T \cap T = T$
18	17 3	eqeltrid	$⊢ φ \to T \cap T \in H$
19		ineq2	$⊢ T = U \to T \cap T = T \cap U$
20	19	eleq1d	$⊢ T = U \to (T \cap T \in H \leftrightarrow T \cap U \in H)$
21	18 20	syl5ibcom	$⊢ φ \to (T = U \to T \cap U \in H)$
22	16 21	impbid	$⊢ φ \to (T \cap U \in H \leftrightarrow T = U)$

Metamath Proof Explorer