Metamath Proof Explorer

Theorem djh02

Description: Closed subspace join with zero. (Contributed by NM, 9-Aug-2014)

Ref Expression
Hypotheses djh01.h 
|- H = ( LHyp ` K )
djh01.u 
|- U = ( ( DVecH ` K ) ` W )
djh01.o 
|- .0. = ( 0g ` U )
djh01.i 
|- I = ( ( DIsoH ` K ) ` W )
djh01.j 
|- .\/ = ( ( joinH ` K ) ` W )
djh01.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
djh01.x 
|- ( ph -> X e. ran I )
Assertion djh02 
|- ( ph -> ( { .0. } .\/ X ) = X )

Proof

Step Hyp Ref Expression
1 djh01.h 
 |-  H = ( LHyp ` K )
2 djh01.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 djh01.o 
 |-  .0. = ( 0g ` U )
4 djh01.i 
 |-  I = ( ( DIsoH ` K ) ` W )
5 djh01.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
6 djh01.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
7 djh01.x 
 |-  ( ph -> X e. ran I )
8 eqid 
 |-  ( Base ` U ) = ( Base ` U )
9 1 4 2 3 dih0rn 
 |-  ( ( K e. HL /\ W e. H ) -> { .0. } e. ran I )
10 1 2 4 8 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { .0. } e. ran I ) -> { .0. } C_ ( Base ` U ) )
11 6 9 10 syl2anc2 
 |-  ( ph -> { .0. } C_ ( Base ` U ) )
12 1 2 4 8 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X C_ ( Base ` U ) )
13 6 7 12 syl2anc 
 |-  ( ph -> X C_ ( Base ` U ) )
14 1 2 8 5 6 11 13 djhcom 
 |-  ( ph -> ( { .0. } .\/ X ) = ( X .\/ { .0. } ) )
15 1 2 3 4 5 6 7 djh01 
 |-  ( ph -> ( X .\/ { .0. } ) = X )
16 14 15 eqtrd 
 |-  ( ph -> ( { .0. } .\/ X ) = X )