# Metamath Proof Explorer

## Theorem dihlss

Description: The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihlss.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dihlss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dihlss.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dihlss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dihlss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion dihlss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 dihlss.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dihlss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dihlss.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dihlss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dihlss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
6 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
7 eqid ${⊢}\mathrm{DIsoB}\left({K}\right)\left({W}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)$
8 1 6 2 3 7 dihvalb ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {X}{\le }_{{K}}{W}\right)\right)\to {I}\left({X}\right)=\mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({X}\right)$
9 1 6 2 4 7 5 diblss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {X}{\le }_{{K}}{W}\right)\right)\to \mathrm{DIsoB}\left({K}\right)\left({W}\right)\left({X}\right)\in {S}$
10 8 9 eqeltrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {X}{\le }_{{K}}{W}\right)\right)\to {I}\left({X}\right)\in {S}$
11 10 anassrs ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\wedge {X}{\le }_{{K}}{W}\right)\to {I}\left({X}\right)\in {S}$
12 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
13 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
14 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
15 eqid ${⊢}\mathrm{DIsoC}\left({K}\right)\left({W}\right)=\mathrm{DIsoC}\left({K}\right)\left({W}\right)$
16 eqid ${⊢}\mathrm{LSSum}\left({U}\right)=\mathrm{LSSum}\left({U}\right)$
17 1 6 12 13 14 2 3 7 15 4 5 16 dihlsscpre ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge ¬{X}{\le }_{{K}}{W}\right)\right)\to {I}\left({X}\right)\in {S}$
18 17 anassrs ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\wedge ¬{X}{\le }_{{K}}{W}\right)\to {I}\left({X}\right)\in {S}$
19 11 18 pm2.61dan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\in {S}$