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 )