Metamath Proof Explorer

Theorem dihjat1

Description: Subspace sum of a closed subspace and an atom. ( pmapjat1 analog.) (Contributed by NM, 1-Oct-2014)

Ref Expression
Hypotheses dihjat1.h 
|- H = ( LHyp ` K )
dihjat1.u 
|- U = ( ( DVecH ` K ) ` W )
dihjat1.v 
|- V = ( Base ` U )
dihjat1.p 
|- .(+) = ( LSSum ` U )
dihjat1.n 
|- N = ( LSpan ` U )
dihjat1.i 
|- I = ( ( DIsoH ` K ) ` W )
dihjat1.j 
|- .\/ = ( ( joinH ` K ) ` W )
dihjat1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dihjat1.x 
|- ( ph -> X e. ran I )
dihjat1.q 
|- ( ph -> T e. V )
Assertion dihjat1 
|- ( ph -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )

Proof

Step Hyp Ref Expression
1 dihjat1.h 
 |-  H = ( LHyp ` K )
2 dihjat1.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dihjat1.v 
 |-  V = ( Base ` U )
4 dihjat1.p 
 |-  .(+) = ( LSSum ` U )
5 dihjat1.n 
 |-  N = ( LSpan ` U )
6 dihjat1.i 
 |-  I = ( ( DIsoH ` K ) ` W )
7 dihjat1.j 
 |-  .\/ = ( ( joinH ` K ) ` W )
8 dihjat1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dihjat1.x 
 |-  ( ph -> X e. ran I )
10 dihjat1.q 
 |-  ( ph -> T e. V )
11 sneq 
 |-  ( T = ( 0g ` U ) -> { T } = { ( 0g ` U ) } )
12 11 fveq2d 
 |-  ( T = ( 0g ` U ) -> ( N ` { T } ) = ( N ` { ( 0g ` U ) } ) )
13 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
14 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
15 14 5 lspsn0 
 |-  ( U e. LMod -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
16 13 15 syl 
 |-  ( ph -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
17 12 16 sylan9eqr 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> ( N ` { T } ) = { ( 0g ` U ) } )
18 17 oveq2d 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> ( X .\/ ( N ` { T } ) ) = ( X .\/ { ( 0g ` U ) } ) )
19 1 2 14 6 7 8 9 djh01 
 |-  ( ph -> ( X .\/ { ( 0g ` U ) } ) = X )
20 19 adantr 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> ( X .\/ { ( 0g ` U ) } ) = X )
21 17 oveq2d 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> ( X .(+) ( N ` { T } ) ) = ( X .(+) { ( 0g ` U ) } ) )
22 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
23 1 2 6 22 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X e. ( LSubSp ` U ) )
24 8 9 23 syl2anc 
 |-  ( ph -> X e. ( LSubSp ` U ) )
25 22 lsssubg 
 |-  ( ( U e. LMod /\ X e. ( LSubSp ` U ) ) -> X e. ( SubGrp ` U ) )
26 13 24 25 syl2anc 
 |-  ( ph -> X e. ( SubGrp ` U ) )
27 14 4 lsm01 
 |-  ( X e. ( SubGrp ` U ) -> ( X .(+) { ( 0g ` U ) } ) = X )
28 26 27 syl 
 |-  ( ph -> ( X .(+) { ( 0g ` U ) } ) = X )
29 28 adantr 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> ( X .(+) { ( 0g ` U ) } ) = X )
30 21 29 eqtr2d 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> X = ( X .(+) ( N ` { T } ) ) )
31 18 20 30 3eqtrd 
 |-  ( ( ph /\ T = ( 0g ` U ) ) -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )
32 8 adantr 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
33 9 adantr 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> X e. ran I )
34 10 anim1i 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( T e. V /\ T =/= ( 0g ` U ) ) )
35 eldifsn 
 |-  ( T e. ( V \ { ( 0g ` U ) } ) <-> ( T e. V /\ T =/= ( 0g ` U ) ) )
36 34 35 sylibr 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> T e. ( V \ { ( 0g ` U ) } ) )
37 1 2 3 4 5 6 7 32 33 14 36 dihjat1lem 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )
38 31 37 pm2.61dane 
 |-  ( ph -> ( X .\/ ( N ` { T } ) ) = ( X .(+) ( N ` { T } ) ) )