Metamath Proof Explorer

Theorem djhlsmat

Description: The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn ; should we directly use dihjat ? (Contributed by NM, 13-Aug-2014)

Ref Expression
Hypotheses djhlsmat.h ⊢ H = LHyp ⁡ K
djhlsmat.u ⊢ U = DVecH ⁡ K ⁡ W
djhlsmat.v ⊢ V = Base U
djhlsmat.p ⊢ ⊕ ˙ = LSSum ⁡ U
djhlsmat.n ⊢ N = LSpan ⁡ U
djhlsmat.i ⊢ I = DIsoH ⁡ K ⁡ W
djhlsmat.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
djhlsmat.k ⊢ φ → K ∈ HL ∧ W ∈ H
djhlsmat.x ⊢ φ → X ∈ V
djhlsmat.y ⊢ φ → Y ∈ V
Assertion djhlsmat ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X ∨ ˙ N ⁡ Y

Proof

Step Hyp Ref Expression
1 djhlsmat.h ⊢ H = LHyp ⁡ K
2 djhlsmat.u ⊢ U = DVecH ⁡ K ⁡ W
3 djhlsmat.v ⊢ V = Base U
4 djhlsmat.p ⊢ ⊕ ˙ = LSSum ⁡ U
5 djhlsmat.n ⊢ N = LSpan ⁡ U
6 djhlsmat.i ⊢ I = DIsoH ⁡ K ⁡ W
7 djhlsmat.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
8 djhlsmat.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 djhlsmat.x ⊢ φ → X ∈ V
10 djhlsmat.y ⊢ φ → Y ∈ V
11 1 2 8 dvhlmod ⊢ φ → U ∈ LMod
12 9 snssd ⊢ φ → X ⊆ V
13 10 snssd ⊢ φ → Y ⊆ V
14 3 5 4 lsmsp2 ⊢ U ∈ LMod ∧ X ⊆ V ∧ Y ⊆ V → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X ∪ Y
15 11 12 13 14 syl3anc ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X ∪ Y
16 df-pr ⊢ X Y = X ∪ Y
17 16 fveq2i ⊢ N ⁡ X Y = N ⁡ X ∪ Y
18 15 17 eqtr4di ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X Y
19 1 2 3 5 6 8 9 10 dihprrn ⊢ φ → N ⁡ X Y ∈ ran ⁡ I
20 18 19 eqeltrd ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∈ ran ⁡ I
21 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
22 3 21 5 lspsncl ⊢ U ∈ LMod ∧ X ∈ V → N ⁡ X ∈ LSubSp ⁡ U
23 11 9 22 syl2anc ⊢ φ → N ⁡ X ∈ LSubSp ⁡ U
24 3 21 5 lspsncl ⊢ U ∈ LMod ∧ Y ∈ V → N ⁡ Y ∈ LSubSp ⁡ U
25 11 10 24 syl2anc ⊢ φ → N ⁡ Y ∈ LSubSp ⁡ U
26 1 2 3 21 4 6 7 8 23 25 djhlsmcl ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∈ ran ⁡ I ↔ N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X ∨ ˙ N ⁡ Y
27 20 26 mpbid ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y = N ⁡ X ∨ ˙ N ⁡ Y