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

Metamath Proof Explorer

Theorem diasslssN

Description: The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses diasslss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
diasslss.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
diasslss.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
diasslss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion diasslssN ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 diasslss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 diasslss.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
3 diasslss.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 diasslss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 1 3 diaf11N ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )
6 f1ocnvfv2 ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) = 𝑥 )
7 5 6 sylan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) = 𝑥 )
8 1 3 diacnvclN ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑥 ) ∈ dom 𝐼 )
9 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
11 9 10 1 3 diaeldm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ◡ 𝐼 ‘ 𝑥 ) ∈ dom 𝐼 ↔ ( ( ◡ 𝐼 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑥 ) ( le ‘ 𝐾 ) 𝑊 ) ) )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ◡ 𝐼 ‘ 𝑥 ) ∈ dom 𝐼 ↔ ( ( ◡ 𝐼 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑥 ) ( le ‘ 𝐾 ) 𝑊 ) ) )
13 8 12 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( ( ◡ 𝐼 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑥 ) ( le ‘ 𝐾 ) 𝑊 ) )
14 9 10 1 2 3 4 dialss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ◡ 𝐼 ‘ 𝑥 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑥 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) ∈ 𝑆 )
15 13 14 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑥 ) ) ∈ 𝑆 )
16 7 15 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ran 𝐼 ) → 𝑥 ∈ 𝑆 )
17 16 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ ran 𝐼 → 𝑥 ∈ 𝑆 ) )
18 17 ssrdv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 )