This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihssxp

Description: An isomorphism H value is included in the vector space (expressed as T X. E ). (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihssxp.b ⊢ B = Base K
dihssxp.h ⊢ H = LHyp ⁡ K
dihssxp.t ⊢ T = LTrn ⁡ K ⁡ W
dihssxp.e ⊢ E = TEndo ⁡ K ⁡ W
dihssxp.i ⊢ I = DIsoH ⁡ K ⁡ W
dihssxp.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihssxp.x ⊢ φ → X ∈ B
Assertion dihssxp ⊢ φ → I ⁡ X ⊆ T × E

Proof

Step Hyp Ref Expression
1 dihssxp.b ⊢ B = Base K
2 dihssxp.h ⊢ H = LHyp ⁡ K
3 dihssxp.t ⊢ T = LTrn ⁡ K ⁡ W
4 dihssxp.e ⊢ E = TEndo ⁡ K ⁡ W
5 dihssxp.i ⊢ I = DIsoH ⁡ K ⁡ W
6 dihssxp.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dihssxp.x ⊢ φ → X ∈ B
8 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
9 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
10 1 2 5 8 9 dihss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
11 6 7 10 syl2anc ⊢ φ → I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
12 2 3 4 8 9 dvhvbase ⊢ K ∈ HL ∧ W ∈ H → Base DVecH ⁡ K ⁡ W = T × E
13 6 12 syl ⊢ φ → Base DVecH ⁡ K ⁡ W = T × E
14 11 13 sseqtrd ⊢ φ → I ⁡ X ⊆ T × E