# Metamath Proof Explorer

## Theorem dih1dimat

Description: Any 1-dimensional subspace is a value of isomorphism H. (Contributed by NM, 11-Apr-2014)

Ref Expression
Hypotheses dih1dimat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dih1dimat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dih1dimat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dih1dimat.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
Assertion dih1dimat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {P}\in {A}\right)\to {P}\in \mathrm{ran}{I}$

### Proof

Step Hyp Ref Expression
1 dih1dimat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dih1dimat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dih1dimat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dih1dimat.a ${⊢}{A}=\mathrm{LSAtoms}\left({U}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
7 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
8 eqid ${⊢}\mathrm{oc}\left({K}\right)\left({W}\right)=\mathrm{oc}\left({K}\right)\left({W}\right)$
9 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
10 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
11 eqid ${⊢}\mathrm{TEndo}\left({K}\right)\left({W}\right)=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
12 eqid ${⊢}\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)=\left({h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)⟼{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\right)$
13 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
14 eqid ${⊢}{inv}_{r}\left(\mathrm{Scalar}\left({U}\right)\right)={inv}_{r}\left(\mathrm{Scalar}\left({U}\right)\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
16 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
17 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
18 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
19 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
20 eqid ${⊢}\left(\iota {h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)|{h}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)={inv}_{r}\left(\mathrm{Scalar}\left({U}\right)\right)\left({s}\right)\left({f}\right)\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\right)=\left(\iota {h}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)|{h}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)={inv}_{r}\left(\mathrm{Scalar}\left({U}\right)\right)\left({s}\right)\left({f}\right)\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\right)$
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {P}\in {A}\right)\to {P}\in \mathrm{ran}{I}$