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 = ( LSHyp ` W )
	lshpin.w	|- ( ph -> W e. LVec )
	lshpin.t	|- ( ph -> T e. H )
	lshpin.u	|- ( ph -> U e. H )
Assertion	lshpinN	|- ( ph -> ( ( T i^i U ) e. H <-> T = U ) )

Proof

Step	Hyp	Ref	Expression
1		lshpin.h	|- H = ( LSHyp ` W )
2		lshpin.w	|- ( ph -> W e. LVec )
3		lshpin.t	|- ( ph -> T e. H )
4		lshpin.u	|- ( ph -> U e. H )
5		inss1	|- ( T i^i U ) C_ T
6	2	adantr	|- ( ( ph /\ ( T i^i U ) e. H ) -> W e. LVec )
7		simpr	|- ( ( ph /\ ( T i^i U ) e. H ) -> ( T i^i U ) e. H )
8	3	adantr	|- ( ( ph /\ ( T i^i U ) e. H ) -> T e. H )
9	1 6 7 8	lshpcmp	|- ( ( ph /\ ( T i^i U ) e. H ) -> ( ( T i^i U ) C_ T <-> ( T i^i U ) = T ) )
10	5 9	mpbii	|- ( ( ph /\ ( T i^i U ) e. H ) -> ( T i^i U ) = T )
11		inss2	|- ( T i^i U ) C_ U
12	4	adantr	|- ( ( ph /\ ( T i^i U ) e. H ) -> U e. H )
13	1 6 7 12	lshpcmp	|- ( ( ph /\ ( T i^i U ) e. H ) -> ( ( T i^i U ) C_ U <-> ( T i^i U ) = U ) )
14	11 13	mpbii	|- ( ( ph /\ ( T i^i U ) e. H ) -> ( T i^i U ) = U )
15	10 14	eqtr3d	|- ( ( ph /\ ( T i^i U ) e. H ) -> T = U )
16	15	ex	|- ( ph -> ( ( T i^i U ) e. H -> T = U ) )
17		inidm	|- ( T i^i T ) = T
18	17 3	eqeltrid	|- ( ph -> ( T i^i T ) e. H )
19		ineq2	|- ( T = U -> ( T i^i T ) = ( T i^i U ) )
20	19	eleq1d	|- ( T = U -> ( ( T i^i T ) e. H <-> ( T i^i U ) e. H ) )
21	18 20	syl5ibcom	|- ( ph -> ( T = U -> ( T i^i U ) e. H ) )
22	16 21	impbid	|- ( ph -> ( ( T i^i U ) e. H <-> T = U ) )