Metamath Proof Explorer

Theorem djhjlj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 9-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 djhjlj ⊢ φ → X J Y = I ⁡ 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 eqid ⊢ Base K = Base K
9 8 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
10 5 6 9 syl2anc ⊢ φ → I -1 ⁡ X ∈ Base K
11 8 2 3 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
12 5 7 11 syl2anc ⊢ φ → I -1 ⁡ Y ∈ Base K
13 8 1 2 3 4 djhlj ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y = I ⁡ I -1 ⁡ X J I ⁡ I -1 ⁡ Y
14 5 10 12 13 syl12anc ⊢ φ → I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y = I ⁡ I -1 ⁡ X J I ⁡ I -1 ⁡ Y
15 2 3 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
16 5 6 15 syl2anc ⊢ φ → I ⁡ I -1 ⁡ X = X
17 2 3 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ Y = Y
18 5 7 17 syl2anc ⊢ φ → I ⁡ I -1 ⁡ Y = Y
19 16 18 oveq12d ⊢ φ → I ⁡ I -1 ⁡ X J I ⁡ I -1 ⁡ Y = X J Y
20 14 19 eqtr2d ⊢ φ → X J Y = I ⁡ I -1 ⁡ X ∨ ˙ I -1 ⁡ Y