Metamath Proof Explorer

Theorem dicssdvh

Description: The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014)

Ref Expression
Hypotheses dicssdvh.l 
|- .<_ = ( le ` K )
dicssdvh.a 
|- A = ( Atoms ` K )
dicssdvh.h 
|- H = ( LHyp ` K )
dicssdvh.i 
|- I = ( ( DIsoC ` K ) ` W )
dicssdvh.u 
|- U = ( ( DVecH ` K ) ` W )
dicssdvh.v 
|- V = ( Base ` U )
Assertion dicssdvh 
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ V )

Proof

Step Hyp Ref Expression
1 dicssdvh.l 
 |-  .<_ = ( le ` K )
2 dicssdvh.a 
 |-  A = ( Atoms ` K )
3 dicssdvh.h 
 |-  H = ( LHyp ` K )
4 dicssdvh.i 
 |-  I = ( ( DIsoC ` K ) ` W )
5 dicssdvh.u 
 |-  U = ( ( DVecH ` K ) ` W )
6 dicssdvh.v 
 |-  V = ( Base ` U )
7 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) )
8 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( K e. HL /\ W e. H ) )
9 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> s e. ( ( TEndo ` K ) ` W ) )
10 eqid 
 |-  ( oc ` K ) = ( oc ` K )
11 1 10 2 3 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
12 11 ad2antrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) )
13 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
14 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
15 eqid 
 |-  ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) = ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q )
16 1 2 3 14 15 ltrniotacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( ( oc ` K ) ` W ) e. A /\ -. ( ( oc ` K ) ` W ) .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
17 8 12 13 16 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) )
18 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
19 3 14 18 tendocl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ s e. ( ( TEndo ` K ) ` W ) /\ ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) e. ( ( LTrn ` K ) ` W ) ) -> ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) e. ( ( LTrn ` K ) ` W ) )
20 8 9 17 19 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) e. ( ( LTrn ` K ) ` W ) )
21 7 20 eqeltrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> f e. ( ( LTrn ` K ) ` W ) )
22 21 9 9 jca31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) )
23 22 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) -> ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) ) )
24 23 ssopab2dv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } C_ { <. f , s >. | ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
25 opabssxp 
 |-  { <. f , s >. | ( ( f e. ( ( LTrn ` K ) ` W ) /\ s e. ( ( TEndo ` K ) ` W ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) )
26 24 25 sstrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
27 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
28 1 2 3 27 14 18 4 dicval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = Q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
29 3 14 18 5 6 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> V = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
30 29 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> V = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
31 26 28 30 3sstr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ V )