Theorem 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=\mathrm{LSHyp}\left(W\right)$$
	lshpin.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lshpin.t	$$⊢\phi \to T\in H$$
	lshpin.u	$$⊢\phi \to U\in H$$
Assertion	lshpinN	$$⊢\phi \to \left(T\cap U\in H\leftrightarrow T=U\right)$$

Proof

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