This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )