Metamath Proof Explorer

Theorem diassdvaN

Description: The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses diassdva.b ⊢ B = Base K
diassdva.l ⊢ ≤ ˙ = ≤ K
diassdva.h ⊢ H = LHyp ⁡ K
diassdva.i ⊢ I = DIsoA ⁡ K ⁡ W
diassdva.u ⊢ U = DVecA ⁡ K ⁡ W
diassdva.v ⊢ V = Base U
Assertion diassdvaN ⊢ K ∈ Y ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X ⊆ V

Proof

Step Hyp Ref Expression
1 diassdva.b ⊢ B = Base K
2 diassdva.l ⊢ ≤ ˙ = ≤ K
3 diassdva.h ⊢ H = LHyp ⁡ K
4 diassdva.i ⊢ I = DIsoA ⁡ K ⁡ W
5 diassdva.u ⊢ U = DVecA ⁡ K ⁡ W
6 diassdva.v ⊢ V = Base U
7 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
8 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
9 1 2 3 7 8 4 diaval ⊢ K ∈ Y ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X
10 ssrab2 ⊢ f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X ⊆ LTrn ⁡ K ⁡ W
11 3 7 5 6 dvavbase ⊢ K ∈ Y ∧ W ∈ H → V = LTrn ⁡ K ⁡ W
12 11 adantr ⊢ K ∈ Y ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → V = LTrn ⁡ K ⁡ W
13 10 12 sseqtrrid ⊢ K ∈ Y ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → f ∈ LTrn ⁡ K ⁡ W | trL ⁡ K ⁡ W ⁡ f ≤ ˙ X ⊆ V
14 9 13 eqsstrd ⊢ K ∈ Y ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X ⊆ V