Metamath Proof Explorer

Theorem lshpcmp

Description: If two hyperplanes are comparable, they are equal. (Contributed by NM, 9-Oct-2014)

Ref Expression
Hypotheses lshpcmp.h 
|- H = ( LSHyp ` W )
lshpcmp.w 
|- ( ph -> W e. LVec )
lshpcmp.t 
|- ( ph -> T e. H )
lshpcmp.u 
|- ( ph -> U e. H )
Assertion lshpcmp 
|- ( ph -> ( T C_ U <-> T = U ) )

Proof

Step Hyp Ref Expression
1 lshpcmp.h 
 |-  H = ( LSHyp ` W )
2 lshpcmp.w 
 |-  ( ph -> W e. LVec )
3 lshpcmp.t 
 |-  ( ph -> T e. H )
4 lshpcmp.u 
 |-  ( ph -> U e. H )
5 eqid 
 |-  ( Base ` W ) = ( Base ` W )
6 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
7 2 6 syl 
 |-  ( ph -> W e. LMod )
8 5 1 7 4 lshpne 
 |-  ( ph -> U =/= ( Base ` W ) )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 9 1 7 4 lshplss 
 |-  ( ph -> U e. ( LSubSp ` W ) )
11 5 9 lssss 
 |-  ( U e. ( LSubSp ` W ) -> U C_ ( Base ` W ) )
12 10 11 syl 
 |-  ( ph -> U C_ ( Base ` W ) )
13 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
14 eqid 
 |-  ( LSSum ` W ) = ( LSSum ` W )
15 5 13 9 14 1 7 islshpsm 
 |-  ( ph -> ( T e. H <-> ( T e. ( LSubSp ` W ) /\ T =/= ( Base ` W ) /\ E. v e. ( Base ` W ) ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) )
16 3 15 mpbid 
 |-  ( ph -> ( T e. ( LSubSp ` W ) /\ T =/= ( Base ` W ) /\ E. v e. ( Base ` W ) ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) )
17 16 simp3d 
 |-  ( ph -> E. v e. ( Base ` W ) ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) )
18 id 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> ( ph /\ v e. ( Base ` W ) ) )
19 18 adantrr 
 |-  ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) -> ( ph /\ v e. ( Base ` W ) ) )
20 2 adantr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> W e. LVec )
21 9 1 7 3 lshplss 
 |-  ( ph -> T e. ( LSubSp ` W ) )
22 21 adantr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> T e. ( LSubSp ` W ) )
23 10 adantr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> U e. ( LSubSp ` W ) )
24 simpr 
 |-  ( ( ph /\ v e. ( Base ` W ) ) -> v e. ( Base ` W ) )
25 5 9 13 14 20 22 23 24 lsmcv 
 |-  ( ( ( ph /\ v e. ( Base ` W ) ) /\ T C. U /\ U C_ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) )
26 19 25 syl3an1 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) /\ T C. U /\ U C_ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) ) -> U = ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) )
27 26 3expia 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) /\ T C. U ) -> ( U C_ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) -> U = ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) ) )
28 simplrr 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) /\ T C. U ) -> ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) )
29 28 sseq2d 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) /\ T C. U ) -> ( U C_ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) <-> U C_ ( Base ` W ) ) )
30 28 eqeq2d 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) /\ T C. U ) -> ( U = ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) <-> U = ( Base ` W ) ) )
31 27 29 30 3imtr3d 
 |-  ( ( ( ph /\ ( v e. ( Base ` W ) /\ ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) ) ) /\ T C. U ) -> ( U C_ ( Base ` W ) -> U = ( Base ` W ) ) )
32 31 exp42 
 |-  ( ph -> ( v e. ( Base ` W ) -> ( ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) -> ( T C. U -> ( U C_ ( Base ` W ) -> U = ( Base ` W ) ) ) ) ) )
33 32 rexlimdv 
 |-  ( ph -> ( E. v e. ( Base ` W ) ( T ( LSSum ` W ) ( ( LSpan ` W ) ` { v } ) ) = ( Base ` W ) -> ( T C. U -> ( U C_ ( Base ` W ) -> U = ( Base ` W ) ) ) ) )
34 17 33 mpd 
 |-  ( ph -> ( T C. U -> ( U C_ ( Base ` W ) -> U = ( Base ` W ) ) ) )
35 12 34 mpid 
 |-  ( ph -> ( T C. U -> U = ( Base ` W ) ) )
36 35 necon3ad 
 |-  ( ph -> ( U =/= ( Base ` W ) -> -. T C. U ) )
37 8 36 mpd 
 |-  ( ph -> -. T C. U )
38 df-pss 
 |-  ( T C. U <-> ( T C_ U /\ T =/= U ) )
39 38 simplbi2 
 |-  ( T C_ U -> ( T =/= U -> T C. U ) )
40 39 necon1bd 
 |-  ( T C_ U -> ( -. T C. U -> T = U ) )
41 37 40 syl5com 
 |-  ( ph -> ( T C_ U -> T = U ) )
42 eqimss 
 |-  ( T = U -> T C_ U )
43 41 42 impbid1 
 |-  ( ph -> ( T C_ U <-> T = U ) )