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

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
diassdva.l ⊢ ≤ = ( le ‘ 𝐾 )
diassdva.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diassdva.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
diassdva.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
diassdva.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
Assertion diassdvaN ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ 𝑉 )

Proof

Step Hyp Ref Expression
1 diassdva.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 diassdva.l ⊢ ≤ = ( le ‘ 𝐾 )
3 diassdva.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 diassdva.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5 diassdva.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
6 diassdva.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
7 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 1 2 3 7 8 4 diaval ⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } )
10 ssrab2 ⊢ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } ⊆ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
11 3 7 5 6 dvavbase ⊢ ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) → 𝑉 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑉 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
13 10 12 sseqtrrid ⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑋 } ⊆ 𝑉 )
14 9 13 eqsstrd ⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ 𝑉 )