Metamath Proof Explorer

Theorem dibss

Description: The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014)

Ref Expression
Hypotheses dibss.b ⊢ B = Base K
dibss.l ⊢ ≤ ˙ = ≤ K
dibss.h ⊢ H = LHyp ⁡ K
dibss.i ⊢ I = DIsoB ⁡ K ⁡ W
dibss.u ⊢ U = DVecH ⁡ K ⁡ W
dibss.v ⊢ V = Base U
Assertion dibss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X ⊆ V

Proof

Step Hyp Ref Expression
1 dibss.b ⊢ B = Base K
2 dibss.l ⊢ ≤ ˙ = ≤ K
3 dibss.h ⊢ H = LHyp ⁡ K
4 dibss.i ⊢ I = DIsoB ⁡ K ⁡ W
5 dibss.u ⊢ U = DVecH ⁡ K ⁡ W
6 dibss.v ⊢ V = Base U
7 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
8 eqid ⊢ DIsoA ⁡ K ⁡ W = DIsoA ⁡ K ⁡ W
9 1 2 3 7 8 diass ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → DIsoA ⁡ K ⁡ W ⁡ X ⊆ LTrn ⁡ K ⁡ W
10 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
11 eqid ⊢ f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B = f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B
12 1 3 7 10 11 tendo0cl ⊢ K ∈ HL ∧ W ∈ H → f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ∈ TEndo ⁡ K ⁡ W
13 12 snssd ⊢ K ∈ HL ∧ W ∈ H → f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ⊆ TEndo ⁡ K ⁡ W
14 13 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ⊆ TEndo ⁡ K ⁡ W
15 xpss12 ⊢ DIsoA ⁡ K ⁡ W ⁡ X ⊆ LTrn ⁡ K ⁡ W ∧ f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ⊆ TEndo ⁡ K ⁡ W → DIsoA ⁡ K ⁡ W ⁡ X × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ⊆ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W
16 9 14 15 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → DIsoA ⁡ K ⁡ W ⁡ X × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B ⊆ LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W
17 1 2 3 7 11 8 4 dibval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = DIsoA ⁡ K ⁡ W ⁡ X × f ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B
18 3 7 10 5 6 dvhvbase ⊢ K ∈ HL ∧ W ∈ H → V = LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W
19 18 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → V = LTrn ⁡ K ⁡ W × TEndo ⁡ K ⁡ W
20 16 17 19 3sstr4d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X ⊆ V