Metamath Proof Explorer

Theorem diclss

Description: The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014)

Ref Expression
Hypotheses diclss.l 
|- .<_ = ( le ` K )
diclss.a 
|- A = ( Atoms ` K )
diclss.h 
|- H = ( LHyp ` K )
diclss.u 
|- U = ( ( DVecH ` K ) ` W )
diclss.i 
|- I = ( ( DIsoC ` K ) ` W )
diclss.s 
|- S = ( LSubSp ` U )
Assertion diclss 
|- ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) e. S )

Proof

Step Hyp Ref Expression
1 diclss.l 
 |-  .<_ = ( le ` K )
2 diclss.a 
 |-  A = ( Atoms ` K )
3 diclss.h 
 |-  H = ( LHyp ` K )
4 diclss.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 diclss.i 
 |-  I = ( ( DIsoC ` K ) ` W )
6 diclss.s 
 |-  S = ( LSubSp ` U )
7 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Scalar ` U ) = ( Scalar ` U ) )
8 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
9 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
10 eqid 
 |-  ( Base ` ( Scalar ` U ) ) = ( Base ` ( Scalar ` U ) )
11 3 8 4 9 10 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( Scalar ` U ) ) = ( ( TEndo ` K ) ` W ) )
12 11 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( TEndo ` K ) ` W ) = ( Base ` ( Scalar ` U ) ) )
13 12 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( TEndo ` K ) ` W ) = ( Base ` ( Scalar ` U ) ) )
14 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
15 eqid 
 |-  ( Base ` U ) = ( Base ` U )
16 3 14 8 4 15 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
17 16 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) = ( Base ` U ) )
18 17 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) = ( Base ` U ) )
19 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( +g ` U ) = ( +g ` U ) )
20 eqidd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( .s ` U ) = ( .s ` U ) )
21 6 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> S = ( LSubSp ` U ) )
22 1 2 3 5 4 15 dicssdvh 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( Base ` U ) )
23 22 18 sseqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
24 1 2 3 5 dicn0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) =/= (/) )
25 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> ( K e. HL /\ W e. H ) )
26 simplr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
27 simpr1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> x e. ( ( TEndo ` K ) ` W ) )
28 simpr2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> a e. ( I ` Q ) )
29 eqid 
 |-  ( .s ` U ) = ( .s ` U )
30 1 2 3 8 4 5 29 dicvscacl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) ) ) -> ( x ( .s ` U ) a ) e. ( I ` Q ) )
31 25 26 27 28 30 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> ( x ( .s ` U ) a ) e. ( I ` Q ) )
32 simpr3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> b e. ( I ` Q ) )
33 eqid 
 |-  ( +g ` U ) = ( +g ` U )
34 1 2 3 4 5 33 dicvaddcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( ( x ( .s ` U ) a ) e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. ( I ` Q ) )
35 25 26 31 32 34 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( x e. ( ( TEndo ` K ) ` W ) /\ a e. ( I ` Q ) /\ b e. ( I ` Q ) ) ) -> ( ( x ( .s ` U ) a ) ( +g ` U ) b ) e. ( I ` Q ) )
36 7 13 18 19 20 21 23 24 35 islssd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) e. S )