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 ⊢ H = LHyp ⁡ K
diasslss.u ⊢ U = DVecA ⁡ K ⁡ W
diasslss.i ⊢ I = DIsoA ⁡ K ⁡ W
diasslss.s ⊢ S = LSubSp ⁡ U
Assertion diasslssN ⊢ K ∈ HL ∧ W ∈ H → ran ⁡ I ⊆ S

Proof

Step Hyp Ref Expression
1 diasslss.h ⊢ H = LHyp ⁡ K
2 diasslss.u ⊢ U = DVecA ⁡ K ⁡ W
3 diasslss.i ⊢ I = DIsoA ⁡ K ⁡ W
4 diasslss.s ⊢ S = LSubSp ⁡ U
5 1 3 diaf11N ⊢ K ∈ HL ∧ W ∈ H → I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I
6 f1ocnvfv2 ⊢ I : dom ⁡ I ⟶ 1-1 onto ran ⁡ I ∧ x ∈ ran ⁡ I → I ⁡ I -1 ⁡ x = x
7 5 6 sylan ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ I → I ⁡ I -1 ⁡ x = x
8 1 3 diacnvclN ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ I → I -1 ⁡ x ∈ dom ⁡ I
9 eqid ⊢ Base K = Base K
10 eqid ⊢ ≤ K = ≤ K
11 9 10 1 3 diaeldm ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ x ∈ dom ⁡ I ↔ I -1 ⁡ x ∈ Base K ∧ I -1 ⁡ x ≤ K W
12 11 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ I → I -1 ⁡ x ∈ dom ⁡ I ↔ I -1 ⁡ x ∈ Base K ∧ I -1 ⁡ x ≤ K W
13 8 12 mpbid ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ I → I -1 ⁡ x ∈ Base K ∧ I -1 ⁡ x ≤ K W
14 9 10 1 2 3 4 dialss ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ x ∈ Base K ∧ I -1 ⁡ x ≤ K W → I ⁡ I -1 ⁡ x ∈ S
15 13 14 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ I → I ⁡ I -1 ⁡ x ∈ S
16 7 15 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ I → x ∈ S
17 16 ex ⊢ K ∈ HL ∧ W ∈ H → x ∈ ran ⁡ I → x ∈ S
18 17 ssrdv ⊢ K ∈ HL ∧ W ∈ H → ran ⁡ I ⊆ S