Metamath Proof Explorer

Theorem djh01

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 djh01 
|- ( ph -> ( X .\/ { .0. } ) = 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 
 |-  ( join ` K ) = ( join ` K )
9 1 4 2 3 dih0rn 
 |-  ( ( K e. HL /\ W e. H ) -> { .0. } e. ran I )
10 6 9 syl 
 |-  ( ph -> { .0. } e. ran I )
11 8 1 4 5 6 7 10 djhjlj 
 |-  ( ph -> ( X .\/ { .0. } ) = ( I ` ( ( `' I ` X ) ( join ` K ) ( `' I ` { .0. } ) ) ) )
12 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
13 1 12 4 2 3 dih0cnv 
 |-  ( ( K e. HL /\ W e. H ) -> ( `' I ` { .0. } ) = ( 0. ` K ) )
14 6 13 syl 
 |-  ( ph -> ( `' I ` { .0. } ) = ( 0. ` K ) )
15 14 oveq2d 
 |-  ( ph -> ( ( `' I ` X ) ( join ` K ) ( `' I ` { .0. } ) ) = ( ( `' I ` X ) ( join ` K ) ( 0. ` K ) ) )
16 6 simpld 
 |-  ( ph -> K e. HL )
17 hlol 
 |-  ( K e. HL -> K e. OL )
18 16 17 syl 
 |-  ( ph -> K e. OL )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 19 1 4 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
21 6 7 20 syl2anc 
 |-  ( ph -> ( `' I ` X ) e. ( Base ` K ) )
22 19 8 12 olj01 
 |-  ( ( K e. OL /\ ( `' I ` X ) e. ( Base ` K ) ) -> ( ( `' I ` X ) ( join ` K ) ( 0. ` K ) ) = ( `' I ` X ) )
23 18 21 22 syl2anc 
 |-  ( ph -> ( ( `' I ` X ) ( join ` K ) ( 0. ` K ) ) = ( `' I ` X ) )
24 15 23 eqtrd 
 |-  ( ph -> ( ( `' I ` X ) ( join ` K ) ( `' I ` { .0. } ) ) = ( `' I ` X ) )
25 24 fveq2d 
 |-  ( ph -> ( I ` ( ( `' I ` X ) ( join ` K ) ( `' I ` { .0. } ) ) ) = ( I ` ( `' I ` X ) ) )
26 1 4 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
27 6 7 26 syl2anc 
 |-  ( ph -> ( I ` ( `' I ` X ) ) = X )
28 11 25 27 3eqtrd 
 |-  ( ph -> ( X .\/ { .0. } ) = X )