Metamath Proof Explorer

Theorem dih1dimat

Description: Any 1-dimensional subspace is a value of isomorphism H. (Contributed by NM, 11-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h 
|- H = ( LHyp ` K )
dih1dimat.u 
|- U = ( ( DVecH ` K ) ` W )
dih1dimat.i 
|- I = ( ( DIsoH ` K ) ` W )
dih1dimat.a 
|- A = ( LSAtoms ` U )
Assertion dih1dimat 
|- ( ( ( K e. HL /\ W e. H ) /\ P e. A ) -> P e. ran I )

Proof

Step Hyp Ref Expression
1 dih1dimat.h 
 |-  H = ( LHyp ` K )
2 dih1dimat.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dih1dimat.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dih1dimat.a 
 |-  A = ( LSAtoms ` U )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
8 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
9 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
10 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
11 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
12 eqid 
 |-  ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) ) = ( h e. ( ( LTrn ` K ) ` W ) |-> ( _I |` ( Base ` K ) ) )
13 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
14 eqid 
 |-  ( invr ` ( Scalar ` U ) ) = ( invr ` ( Scalar ` U ) )
15 eqid 
 |-  ( Base ` U ) = ( Base ` U )
16 eqid 
 |-  ( .s ` U ) = ( .s ` U )
17 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
18 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
19 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
20 eqid 
 |-  ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = ( ( ( ( invr ` ( Scalar ` U ) ) ` s ) ` f ) ` ( ( oc ` K ) ` W ) ) ) = ( iota_ h e. ( ( LTrn ` K ) ` W ) ( h ` ( ( oc ` K ) ` W ) ) = ( ( ( ( invr ` ( Scalar ` U ) ) ` s ) ` f ) ` ( ( oc ` K ) ` W ) ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem 
 |-  ( ( ( K e. HL /\ W e. H ) /\ P e. A ) -> P e. ran I )