# 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
diclss.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
diclss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
diclss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
diclss.i ${⊢}{I}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
diclss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion diclss

### Proof

Step Hyp Ref Expression
1 diclss.l
2 diclss.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 diclss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 diclss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 diclss.i ${⊢}{I}=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
6 diclss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
7 eqidd
8 eqid ${⊢}\mathrm{TEndo}\left({K}\right)\left({W}\right)=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
9 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
10 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}$
11 3 8 4 9 10 dvhbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
12 11 eqcomd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{TEndo}\left({K}\right)\left({W}\right)={\mathrm{Base}}_{\mathrm{Scalar}\left({U}\right)}$
13 12 adantr
14 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
16 3 14 8 4 15 dvhvbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{U}}=\mathrm{LTrn}\left({K}\right)\left({W}\right)×\mathrm{TEndo}\left({K}\right)\left({W}\right)$
17 16 eqcomd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{LTrn}\left({K}\right)\left({W}\right)×\mathrm{TEndo}\left({K}\right)\left({W}\right)={\mathrm{Base}}_{{U}}$
18 17 adantr
19 eqidd
20 eqidd
21 6 a1i
22 1 2 3 5 4 15 dicssdvh
23 22 18 sseqtrrd
24 1 2 3 5 dicn0
25 simpll
26 simplr
27 simpr1
28 simpr2
29 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
30 1 2 3 8 4 5 29 dicvscacl
31 25 26 27 28 30 syl112anc
32 simpr3
33 eqid ${⊢}{+}_{{U}}={+}_{{U}}$
34 1 2 3 4 5 33 dicvaddcl
35 25 26 31 32 34 syl112anc
36 7 13 18 19 20 21 23 24 35 islssd