This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihsumssj

Description: The subspace sum of two isomorphisms of lattice elements is less than the isomorphism of their lattice join. (Contributed by NM, 23-Sep-2014)

Ref Expression
Hypotheses dihsumssj.b ⊢ B = Base K
dihsumssj.h ⊢ H = LHyp ⁡ K
dihsumssj.j ⊢ ∨ ˙ = join ⁡ K
dihsumssj.u ⊢ U = DVecH ⁡ K ⁡ W
dihsumssj.p ⊢ ⊕ ˙ = LSSum ⁡ U
dihsumssj.i ⊢ I = DIsoH ⁡ K ⁡ W
dihsumssj.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihsumssj.x ⊢ φ → X ∈ B
dihsumssj.y ⊢ φ → Y ∈ B
Assertion dihsumssj ⊢ φ → I ⁡ X ⊕ ˙ I ⁡ Y ⊆ I ⁡ X ∨ ˙ Y

Proof

Step Hyp Ref Expression
1 dihsumssj.b ⊢ B = Base K
2 dihsumssj.h ⊢ H = LHyp ⁡ K
3 dihsumssj.j ⊢ ∨ ˙ = join ⁡ K
4 dihsumssj.u ⊢ U = DVecH ⁡ K ⁡ W
5 dihsumssj.p ⊢ ⊕ ˙ = LSSum ⁡ U
6 dihsumssj.i ⊢ I = DIsoH ⁡ K ⁡ W
7 dihsumssj.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dihsumssj.x ⊢ φ → X ∈ B
9 dihsumssj.y ⊢ φ → Y ∈ B
10 eqid ⊢ Base U = Base U
11 eqid ⊢ joinH ⁡ K ⁡ W = joinH ⁡ K ⁡ W
12 1 2 6 4 10 dihss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ⊆ Base U
13 7 8 12 syl2anc ⊢ φ → I ⁡ X ⊆ Base U
14 1 2 6 4 10 dihss ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ B → I ⁡ Y ⊆ Base U
15 7 9 14 syl2anc ⊢ φ → I ⁡ Y ⊆ Base U
16 2 4 10 5 11 7 13 15 djhsumss ⊢ φ → I ⁡ X ⊕ ˙ I ⁡ Y ⊆ I ⁡ X joinH ⁡ K ⁡ W I ⁡ Y
17 1 3 2 6 11 djhlj ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∨ ˙ Y = I ⁡ X joinH ⁡ K ⁡ W I ⁡ Y
18 7 8 9 17 syl12anc ⊢ φ → I ⁡ X ∨ ˙ Y = I ⁡ X joinH ⁡ K ⁡ W I ⁡ Y
19 16 18 sseqtrrd ⊢ φ → I ⁡ X ⊕ ˙ I ⁡ Y ⊆ I ⁡ X ∨ ˙ Y