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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihssxp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihssxp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dihssxp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dihssxp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihssxp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihssxp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion dihssxp ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝑇 × 𝐸 ) )

Proof

Step Hyp Ref Expression
1 dihssxp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihssxp.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihssxp.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dihssxp.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5 dihssxp.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
6 dihssxp.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dihssxp.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
10 1 2 5 8 9 dihss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
11 6 7 10 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
12 2 3 4 8 9 dvhvbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑇 × 𝐸 ) )
13 6 12 syl ⊢ ( 𝜑 → ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑇 × 𝐸 ) )
14 11 13 sseqtrd ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝑇 × 𝐸 ) )