Metamath Proof Explorer

Theorem djhljjN

Description: Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 djhlj.b ⊢ B = Base K
2 djhlj.k ⊢ ∨ ˙ = join ⁡ K
3 djhlj.h ⊢ H = LHyp ⁡ K
4 djhlj.i ⊢ I = DIsoH ⁡ K ⁡ W
5 djhlj.j ⊢ J = joinH ⁡ K ⁡ W
6 djhljj.w ⊢ φ → K ∈ HL ∧ W ∈ H
7 djhljj.x ⊢ φ → X ∈ B
8 djhljj.y ⊢ φ → Y ∈ B
9 1 2 3 4 5 djhlj ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∨ ˙ Y = I ⁡ X J I ⁡ Y
10 6 7 8 9 syl12anc ⊢ φ → I ⁡ X ∨ ˙ Y = I ⁡ X J I ⁡ Y
11 1 3 4 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ∈ ran ⁡ I
12 6 7 11 syl2anc ⊢ φ → I ⁡ X ∈ ran ⁡ I
13 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
14 eqid ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
15 3 13 4 14 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ I ⁡ X ∈ ran ⁡ I → I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
16 6 12 15 syl2anc ⊢ φ → I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
17 1 3 4 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B → I ⁡ Y ∈ ran ⁡ I
18 6 8 17 syl2anc ⊢ φ → I ⁡ Y ∈ ran ⁡ I
19 3 13 4 14 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ I ⁡ Y ∈ ran ⁡ I → I ⁡ Y ⊆ Base DVecH ⁡ K ⁡ W
20 6 18 19 syl2anc ⊢ φ → I ⁡ Y ⊆ Base DVecH ⁡ K ⁡ W
21 3 4 13 14 5 djhcl ⊢ K ∈ HL ∧ W ∈ H ∧ I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W ∧ I ⁡ Y ⊆ Base DVecH ⁡ K ⁡ W → I ⁡ X J I ⁡ Y ∈ ran ⁡ I
22 6 16 20 21 syl12anc ⊢ φ → I ⁡ X J I ⁡ Y ∈ ran ⁡ I
23 3 4 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ I ⁡ X J I ⁡ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ I ⁡ X J I ⁡ Y = I ⁡ X J I ⁡ Y
24 6 22 23 syl2anc ⊢ φ → I ⁡ I -1 ⁡ I ⁡ X J I ⁡ Y = I ⁡ X J I ⁡ Y
25 10 24 eqtr4d ⊢ φ → I ⁡ X ∨ ˙ Y = I ⁡ I -1 ⁡ I ⁡ X J I ⁡ Y
26 6 simpld ⊢ φ → K ∈ HL
27 26 hllatd ⊢ φ → K ∈ Lat
28 1 2 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B
29 27 7 8 28 syl3anc ⊢ φ → X ∨ ˙ Y ∈ B
30 1 3 4 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ I ⁡ X J I ⁡ Y ∈ ran ⁡ I → I -1 ⁡ I ⁡ X J I ⁡ Y ∈ B
31 6 22 30 syl2anc ⊢ φ → I -1 ⁡ I ⁡ X J I ⁡ Y ∈ B
32 1 3 4 dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∨ ˙ Y ∈ B ∧ I -1 ⁡ I ⁡ X J I ⁡ Y ∈ B → I ⁡ X ∨ ˙ Y = I ⁡ I -1 ⁡ I ⁡ X J I ⁡ Y ↔ X ∨ ˙ Y = I -1 ⁡ I ⁡ X J I ⁡ Y
33 6 29 31 32 syl3anc ⊢ φ → I ⁡ X ∨ ˙ Y = I ⁡ I -1 ⁡ I ⁡ X J I ⁡ Y ↔ X ∨ ˙ Y = I -1 ⁡ I ⁡ X J I ⁡ Y
34 25 33 mpbid ⊢ φ → X ∨ ˙ Y = I -1 ⁡ I ⁡ X J I ⁡ Y