# Metamath Proof Explorer

## Theorem diasslssN

Description: The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses diasslss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
diasslss.u ${⊢}{U}=\mathrm{DVecA}\left({K}\right)\left({W}\right)$
diasslss.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
diasslss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
Assertion diasslssN ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ran}{I}\subseteq {S}$

### Proof

Step Hyp Ref Expression
1 diasslss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 diasslss.u ${⊢}{U}=\mathrm{DVecA}\left({K}\right)\left({W}\right)$
3 diasslss.i ${⊢}{I}=\mathrm{DIsoA}\left({K}\right)\left({W}\right)$
4 diasslss.s ${⊢}{S}=\mathrm{LSubSp}\left({U}\right)$
5 1 3 diaf11N ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}$
6 f1ocnvfv2 ${⊢}\left({I}:\mathrm{dom}{I}\underset{1-1 onto}{⟶}\mathrm{ran}{I}\wedge {x}\in \mathrm{ran}{I}\right)\to {I}\left({{I}}^{-1}\left({x}\right)\right)={x}$
7 5 6 sylan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in \mathrm{ran}{I}\right)\to {I}\left({{I}}^{-1}\left({x}\right)\right)={x}$
8 1 3 diacnvclN ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({x}\right)\in \mathrm{dom}{I}$
9 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
10 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
11 9 10 1 3 diaeldm ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({{I}}^{-1}\left({x}\right)\in \mathrm{dom}{I}↔\left({{I}}^{-1}\left({x}\right)\in {\mathrm{Base}}_{{K}}\wedge {{I}}^{-1}\left({x}\right){\le }_{{K}}{W}\right)\right)$
12 11 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in \mathrm{ran}{I}\right)\to \left({{I}}^{-1}\left({x}\right)\in \mathrm{dom}{I}↔\left({{I}}^{-1}\left({x}\right)\in {\mathrm{Base}}_{{K}}\wedge {{I}}^{-1}\left({x}\right){\le }_{{K}}{W}\right)\right)$
13 8 12 mpbid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in \mathrm{ran}{I}\right)\to \left({{I}}^{-1}\left({x}\right)\in {\mathrm{Base}}_{{K}}\wedge {{I}}^{-1}\left({x}\right){\le }_{{K}}{W}\right)$
14 9 10 1 2 3 4 dialss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({{I}}^{-1}\left({x}\right)\in {\mathrm{Base}}_{{K}}\wedge {{I}}^{-1}\left({x}\right){\le }_{{K}}{W}\right)\right)\to {I}\left({{I}}^{-1}\left({x}\right)\right)\in {S}$
15 13 14 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in \mathrm{ran}{I}\right)\to {I}\left({{I}}^{-1}\left({x}\right)\right)\in {S}$
16 7 15 eqeltrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {x}\in \mathrm{ran}{I}\right)\to {x}\in {S}$
17 16 ex ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({x}\in \mathrm{ran}{I}\to {x}\in {S}\right)$
18 17 ssrdv ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{ran}{I}\subseteq {S}$