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=LHyp⁡K
dih1dimat.u ⊢U=DVecH⁡K⁡W
dih1dimat.i ⊢I=DIsoH⁡K⁡W
dih1dimat.a ⊢A=LSAtoms⁡U
Assertion dih1dimat ⊢K∈HL∧W∈H∧P∈A→P∈ran⁡I

Proof

Step Hyp Ref Expression
1 dih1dimat.h ⊢H=LHyp⁡K
2 dih1dimat.u ⊢U=DVecH⁡K⁡W
3 dih1dimat.i ⊢I=DIsoH⁡K⁡W
4 dih1dimat.a ⊢A=LSAtoms⁡U
5 eqid ⊢BaseK=BaseK
6 eqid ⊢≤K=≤K
7 eqid ⊢Atoms⁡K=Atoms⁡K
8 eqid ⊢oc⁡K⁡W=oc⁡K⁡W
9 eqid ⊢LTrn⁡K⁡W=LTrn⁡K⁡W
10 eqid ⊢trL⁡K⁡W=trL⁡K⁡W
11 eqid ⊢TEndo⁡K⁡W=TEndo⁡K⁡W
12 eqid ⊢h∈LTrn⁡K⁡W⟼I↾BaseK=h∈LTrn⁡K⁡W⟼I↾BaseK
13 eqid ⊢Scalar⁡U=Scalar⁡U
14 eqid ⊢invr⁡Scalar⁡U=invr⁡Scalar⁡U
15 eqid ⊢BaseU=BaseU
16 eqid ⊢⋅U=⋅U
17 eqid ⊢LSubSp⁡U=LSubSp⁡U
18 eqid ⊢LSpan⁡U=LSpan⁡U
19 eqid ⊢0U=0U
20 eqid ⊢ιh∈LTrn⁡K⁡W|h⁡oc⁡K⁡W=invr⁡Scalar⁡U⁡s⁡f⁡oc⁡K⁡W=ιh∈LTrn⁡K⁡W|h⁡oc⁡K⁡W=invr⁡Scalar⁡U⁡s⁡f⁡oc⁡K⁡W
21 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dih1dimatlem ⊢K∈HL∧W∈H∧P∈A→P∈ran⁡I