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 ) |