# 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}=\mathrm{LHyp}\left({K}\right)$
djhlsmat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
djhlsmat.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
djhlsmat.p
djhlsmat.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
djhlsmat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
djhlsmat.j
djhlsmat.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
djhlsmat.x ${⊢}{\phi }\to {X}\in {V}$
djhlsmat.y ${⊢}{\phi }\to {Y}\in {V}$
Assertion djhlsmat

### Proof

Step Hyp Ref Expression
1 djhlsmat.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 djhlsmat.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 djhlsmat.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 djhlsmat.p
5 djhlsmat.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
6 djhlsmat.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
7 djhlsmat.j
8 djhlsmat.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
9 djhlsmat.x ${⊢}{\phi }\to {X}\in {V}$
10 djhlsmat.y ${⊢}{\phi }\to {Y}\in {V}$
11 1 2 8 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
12 9 snssd ${⊢}{\phi }\to \left\{{X}\right\}\subseteq {V}$
13 10 snssd ${⊢}{\phi }\to \left\{{Y}\right\}\subseteq {V}$
14 3 5 4 lsmsp2
15 11 12 13 14 syl3anc
16 df-pr ${⊢}\left\{{X},{Y}\right\}=\left\{{X}\right\}\cup \left\{{Y}\right\}$
17 16 fveq2i ${⊢}{N}\left(\left\{{X},{Y}\right\}\right)={N}\left(\left\{{X}\right\}\cup \left\{{Y}\right\}\right)$
18 15 17 syl6eqr
19 1 2 3 5 6 8 9 10 dihprrn ${⊢}{\phi }\to {N}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{ran}{I}$
20 18 19 eqeltrd
21 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
22 3 21 5 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
23 11 9 22 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
24 3 21 5 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {Y}\in {V}\right)\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
25 11 10 24 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{Y}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
26 1 2 3 21 4 6 7 8 23 25 djhlsmcl
27 20 26 mpbid