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	⊢ ( ( ( 𝐾 ∈ 𝑌 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ 𝑉 )