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 ⊢ Base K = Base K
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 ↾ Base K = h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
13 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
14 eqid ⊢ inv r ⁡ Scalar ⁡ U = inv r ⁡ Scalar ⁡ U
15 eqid ⊢ Base U = Base U
16 eqid ⊢ ⋅ U = ⋅ U
17 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
18 eqid ⊢ LSpan ⁡ U = LSpan ⁡ U
19 eqid ⊢ 0 U = 0 U
20 eqid ⊢ ι h ∈ LTrn ⁡ K ⁡ W | h ⁡ oc ⁡ K ⁡ W = inv r ⁡ Scalar ⁡ U ⁡ s ⁡ f ⁡ oc ⁡ K ⁡ W = ι h ∈ LTrn ⁡ K ⁡ W | h ⁡ oc ⁡ K ⁡ W = inv r ⁡ 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