Metamath Proof Explorer

Theorem dihlss

Description: The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihlss.b ⊢ B = Base K
dihlss.h ⊢ H = LHyp ⁡ K
dihlss.i ⊢ I = DIsoH ⁡ K ⁡ W
dihlss.u ⊢ U = DVecH ⁡ K ⁡ W
dihlss.s ⊢ S = LSubSp ⁡ U
Assertion dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ∈ S

Proof

Step Hyp Ref Expression
1 dihlss.b ⊢ B = Base K
2 dihlss.h ⊢ H = LHyp ⁡ K
3 dihlss.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dihlss.u ⊢ U = DVecH ⁡ K ⁡ W
5 dihlss.s ⊢ S = LSubSp ⁡ U
6 eqid ⊢ ≤ K = ≤ K
7 eqid ⊢ DIsoB ⁡ K ⁡ W = DIsoB ⁡ K ⁡ W
8 1 6 2 3 7 dihvalb ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ K W → I ⁡ X = DIsoB ⁡ K ⁡ W ⁡ X
9 1 6 2 4 7 5 diblss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ K W → DIsoB ⁡ K ⁡ W ⁡ X ∈ S
10 8 9 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ K W → I ⁡ X ∈ S
11 10 anassrs ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ X ≤ K W → I ⁡ X ∈ S
12 eqid ⊢ join ⁡ K = join ⁡ K
13 eqid ⊢ meet ⁡ K = meet ⁡ K
14 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
15 eqid ⊢ DIsoC ⁡ K ⁡ W = DIsoC ⁡ K ⁡ W
16 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
17 1 6 12 13 14 2 3 7 15 4 5 16 dihlsscpre ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ K W → I ⁡ X ∈ S
18 17 anassrs ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ K W → I ⁡ X ∈ S
19 11 18 pm2.61dan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ∈ S