Metamath Proof Explorer

Theorem djhj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses djhj.k ⊢ ∨ ˙ = join ⁡ K
djhj.h ⊢ H = LHyp ⁡ K
djhj.i ⊢ I = DIsoH ⁡ K ⁡ W
djhj.j ⊢ J = joinH ⁡ K ⁡ W
djhj.w ⊢ φ → K ∈ HL ∧ W ∈ H
djhj.x ⊢ φ → X ∈ ran ⁡ I
djhj.y ⊢ φ → Y ∈ ran ⁡ I
Assertion djhj ⊢ φ → I -1 ⁡ X J Y = I -1 ⁡ X ∨ ˙ I -1 ⁡ Y

Proof

Step Hyp Ref Expression
1 djhj.k ⊢ ∨ ˙ = join ⁡ K
2 djhj.h ⊢ H = LHyp ⁡ K
3 djhj.i ⊢ I = DIsoH ⁡ K ⁡ W
4 djhj.j ⊢ J = joinH ⁡ K ⁡ W
5 djhj.w ⊢ φ → K ∈ HL ∧ W ∈ H
6 djhj.x ⊢ φ → X ∈ ran ⁡ I
7 djhj.y ⊢ φ → Y ∈ ran ⁡ I
8 1 2 3 4 5 6 7 djhjlj ⊢ φ → X J Y = I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y
9 8 fveq2d ⊢ φ → I -1 ⁡ X J Y = I -1 ⁡ I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y
10 5 simpld ⊢ φ → K ∈ HL
11 10 hllatd ⊢ φ → K ∈ Lat
12 eqid ⊢ Base K = Base K
13 12 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
14 5 6 13 syl2anc ⊢ φ → I -1 ⁡ X ∈ Base K
15 12 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
16 5 7 15 syl2anc ⊢ φ → I -1 ⁡ Y ∈ Base K
17 12 1 latjcl ⊢ K ∈ Lat ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I -1 ⁡ X ∨ ˙ I -1 ⁡ Y ∈ Base K
18 11 14 16 17 syl3anc ⊢ φ → I -1 ⁡ X ∨ ˙ I -1 ⁡ Y ∈ Base K
19 12 2 3 dihcnvid1 ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y ∈ Base K → I -1 ⁡ I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y = I -1 ⁡ X ∨ ˙ I -1 ⁡ Y
20 5 18 19 syl2anc ⊢ φ → I -1 ⁡ I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y = I -1 ⁡ X ∨ ˙ I -1 ⁡ Y
21 9 20 eqtrd ⊢ φ → I -1 ⁡ X J Y = I -1 ⁡ X ∨ ˙ I -1 ⁡ Y