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 syl6eqr φ 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