Metamath Proof Explorer

Theorem dihlspsnssN

Description: A subspace included in a 1-dim subspace belongs to the range of isomorphism H. (Contributed by NM, 26-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dih1dor0.h 
|- H = ( LHyp ` K )
dih1dor0.u 
|- U = ( ( DVecH ` K ) ` W )
dihldor0.v 
|- V = ( Base ` U )
dih1dor0.s 
|- S = ( LSubSp ` U )
dih1dor0.n 
|- N = ( LSpan ` U )
dih1dor0.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihlspsnssN 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> ( T e. S <-> T e. ran I ) )

Proof

Step Hyp Ref Expression
1 dih1dor0.h 
 |-  H = ( LHyp ` K )
2 dih1dor0.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dihldor0.v 
 |-  V = ( Base ` U )
4 dih1dor0.s 
 |-  S = ( LSubSp ` U )
5 dih1dor0.n 
 |-  N = ( LSpan ` U )
6 dih1dor0.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = ( N ` { X } ) ) -> T = ( N ` { X } ) )
8 1 2 3 5 6 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V ) -> ( N ` { X } ) e. ran I )
9 8 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> ( N ` { X } ) e. ran I )
10 9 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = ( N ` { X } ) ) -> ( N ` { X } ) e. ran I )
11 7 10 eqeltrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = ( N ` { X } ) ) -> T e. ran I )
12 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> T = { ( 0g ` U ) } )
13 simpll1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> ( K e. HL /\ W e. H ) )
14 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
15 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
16 14 1 6 2 15 dih0 
 |-  ( ( K e. HL /\ W e. H ) -> ( I ` ( 0. ` K ) ) = { ( 0g ` U ) } )
17 13 16 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> ( I ` ( 0. ` K ) ) = { ( 0g ` U ) } )
18 12 17 eqtr4d 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> T = ( I ` ( 0. ` K ) ) )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 19 1 6 dihfn 
 |-  ( ( K e. HL /\ W e. H ) -> I Fn ( Base ` K ) )
21 13 20 syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> I Fn ( Base ` K ) )
22 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> K e. HL )
23 22 ad2antrr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> K e. HL )
24 hlop 
 |-  ( K e. HL -> K e. OP )
25 19 14 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. ( Base ` K ) )
26 23 24 25 3syl 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> ( 0. ` K ) e. ( Base ` K ) )
27 fnfvelrn 
 |-  ( ( I Fn ( Base ` K ) /\ ( 0. ` K ) e. ( Base ` K ) ) -> ( I ` ( 0. ` K ) ) e. ran I )
28 21 26 27 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> ( I ` ( 0. ` K ) ) e. ran I )
29 18 28 eqeltrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) /\ T = { ( 0g ` U ) } ) -> T e. ran I )
30 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> ( K e. HL /\ W e. H ) )
31 1 2 30 dvhlvec 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> U e. LVec )
32 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> T e. S )
33 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> X e. V )
34 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> T C_ ( N ` { X } ) )
35 3 15 4 5 lspsnat 
 |-  ( ( ( U e. LVec /\ T e. S /\ X e. V ) /\ T C_ ( N ` { X } ) ) -> ( T = ( N ` { X } ) \/ T = { ( 0g ` U ) } ) )
36 31 32 33 34 35 syl31anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> ( T = ( N ` { X } ) \/ T = { ( 0g ` U ) } ) )
37 11 29 36 mpjaodan 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) /\ T e. S ) -> T e. ran I )
38 37 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> ( T e. S -> T e. ran I ) )
39 1 2 6 4 dihsslss 
 |-  ( ( K e. HL /\ W e. H ) -> ran I C_ S )
40 39 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> ran I C_ S )
41 40 sseld 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> ( T e. ran I -> T e. S ) )
42 38 41 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. V /\ T C_ ( N ` { X } ) ) -> ( T e. S <-> T e. ran I ) )