Metamath Proof Explorer

Theorem djhlsmcl

Description: A closed subspace sum equals subspace join. ( shjshseli analog.) (Contributed by NM, 13-Aug-2014)

Ref Expression
Hypotheses djhlsmcl.h 
|- H = ( LHyp ` K )
djhlsmcl.u 
|- U = ( ( DVecH ` K ) ` W )
djhlsmcl.v 
|- V = ( Base ` U )
djhlsmcl.s 
|- S = ( LSubSp ` U )
djhlsmcl.p 
|- .(+) = ( LSSum ` U )
djhlsmcl.i 
|- I = ( ( DIsoH ` K ) ` W )
djhlsmcl.j 
|- .\/ = ( ( joinH ` K ) ` W )
djhlsmcl.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
djhlsmcl.x 
|- ( ph -> X e. S )
djhlsmcl.y 
|- ( ph -> Y e. S )
Assertion djhlsmcl 
|- ( ph -> ( ( X .(+) Y ) e. ran I <-> ( X .(+) Y ) = ( X .\/ Y ) ) )

Proof

Step Hyp Ref Expression
1 djhlsmcl.h 
 |-  H = ( LHyp ` K )
2 djhlsmcl.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 djhlsmcl.v 
 |-  V = ( Base ` U )
4 djhlsmcl.s 
 |-  S = ( LSubSp ` U )
5 djhlsmcl.p 
 |-  .(+) = ( LSSum ` U )
6 djhlsmcl.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 djhlsmcl.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
8 djhlsmcl.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 djhlsmcl.x 
 |-  ( ph -> X e. S )
10 djhlsmcl.y 
 |-  ( ph -> Y e. S )
11 8 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( K e. HL /\ W e. H ) )
12 3 4 lssss 
 |-  ( X e. S -> X C_ V )
13 9 12 syl 
 |-  ( ph -> X C_ V )
14 13 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> X C_ V )
15 3 4 lssss 
 |-  ( Y e. S -> Y C_ V )
16 10 15 syl 
 |-  ( ph -> Y C_ V )
17 16 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> Y C_ V )
18 eqid 
 |-  ( ( ocH ` K ) ` W ) = ( ( ocH ` K ) ` W )
19 1 2 3 18 7 djhval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V /\ Y C_ V ) -> ( X .\/ Y ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
20 11 14 17 19 syl3anc 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( X .\/ Y ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
21 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
22 21 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> U e. LMod )
23 9 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> X e. S )
24 10 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> Y e. S )
25 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
26 4 25 5 lsmsp 
 |-  ( ( U e. LMod /\ X e. S /\ Y e. S ) -> ( X .(+) Y ) = ( ( LSpan ` U ) ` ( X u. Y ) ) )
27 22 23 24 26 syl3anc 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( X .(+) Y ) = ( ( LSpan ` U ) ` ( X u. Y ) ) )
28 27 fveq2d 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` ( X .(+) Y ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( LSpan ` U ) ` ( X u. Y ) ) ) )
29 13 16 unssd 
 |-  ( ph -> ( X u. Y ) C_ V )
30 29 adantr 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( X u. Y ) C_ V )
31 1 2 18 3 25 11 30 dochocsp 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` ( ( LSpan ` U ) ` ( X u. Y ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) )
32 28 31 eqtrd 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` ( X .(+) Y ) ) = ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) )
33 32 fveq2d 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X .(+) Y ) ) ) = ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X u. Y ) ) ) )
34 1 6 18 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X .(+) Y ) e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X .(+) Y ) ) ) = ( X .(+) Y ) )
35 8 34 sylan 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( ( ( ocH ` K ) ` W ) ` ( ( ( ocH ` K ) ` W ) ` ( X .(+) Y ) ) ) = ( X .(+) Y ) )
36 20 33 35 3eqtr2rd 
 |-  ( ( ph /\ ( X .(+) Y ) e. ran I ) -> ( X .(+) Y ) = ( X .\/ Y ) )
37 36 ex 
 |-  ( ph -> ( ( X .(+) Y ) e. ran I -> ( X .(+) Y ) = ( X .\/ Y ) ) )
38 1 6 2 3 7 djhcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( X C_ V /\ Y C_ V ) ) -> ( X .\/ Y ) e. ran I )
39 8 13 16 38 syl12anc 
 |-  ( ph -> ( X .\/ Y ) e. ran I )
40 eleq1a 
 |-  ( ( X .\/ Y ) e. ran I -> ( ( X .(+) Y ) = ( X .\/ Y ) -> ( X .(+) Y ) e. ran I ) )
41 39 40 syl 
 |-  ( ph -> ( ( X .(+) Y ) = ( X .\/ Y ) -> ( X .(+) Y ) e. ran I ) )
42 37 41 impbid 
 |-  ( ph -> ( ( X .(+) Y ) e. ran I <-> ( X .(+) Y ) = ( X .\/ Y ) ) )