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

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 
|- ( ph -> ( K e. HL /\ W e. H ) )
djhlsmat.x 
|- ( ph -> X e. V )
djhlsmat.y 
|- ( ph -> Y e. V )
Assertion djhlsmat 
|- ( ph -> ( ( 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 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 djhlsmat.x 
 |-  ( ph -> X e. V )
10 djhlsmat.y 
 |-  ( ph -> Y e. V )
11 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
12 9 snssd 
 |-  ( ph -> { X } C_ V )
13 10 snssd 
 |-  ( ph -> { Y } C_ V )
14 3 5 4 lsmsp2 
 |-  ( ( U e. LMod /\ { X } C_ V /\ { Y } C_ V ) -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
15 11 12 13 14 syl3anc 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` ( { X } u. { Y } ) ) )
16 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
17 16 fveq2i 
 |-  ( N ` { X , Y } ) = ( N ` ( { X } u. { Y } ) )
18 15 17 eqtr4di 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( N ` { X , Y } ) )
19 1 2 3 5 6 8 9 10 dihprrn 
 |-  ( ph -> ( N ` { X , Y } ) e. ran I )
20 18 19 eqeltrd 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ran I )
21 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
22 3 21 5 lspsncl 
 |-  ( ( U e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` U ) )
23 11 9 22 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` U ) )
24 3 21 5 lspsncl 
 |-  ( ( U e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` U ) )
25 11 10 24 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` U ) )
26 1 2 3 21 4 6 7 8 23 25 djhlsmcl 
 |-  ( ph -> ( ( ( N ` { X } ) .(+) ( N ` { Y } ) ) e. ran I <-> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( ( N ` { X } ) .\/ ( N ` { Y } ) ) ) )
27 20 26 mpbid 
 |-  ( ph -> ( ( N ` { X } ) .(+) ( N ` { Y } ) ) = ( ( N ` { X } ) .\/ ( N ` { Y } ) ) )