Metamath Proof Explorer

Theorem hdmap10

Description: Part 10 in Baer p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015)

Ref Expression
Hypotheses hdmap10.h 
|- H = ( LHyp ` K )
hdmap10.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap10.v 
|- V = ( Base ` U )
hdmap10.n 
|- N = ( LSpan ` U )
hdmap10.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap10.l 
|- L = ( LSpan ` C )
hdmap10.m 
|- M = ( ( mapd ` K ) ` W )
hdmap10.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap10.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap10.t 
|- ( ph -> T e. V )
Assertion hdmap10 
|- ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )

Proof

Step Hyp Ref Expression
1 hdmap10.h 
 |-  H = ( LHyp ` K )
2 hdmap10.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap10.v 
 |-  V = ( Base ` U )
4 hdmap10.n 
 |-  N = ( LSpan ` U )
5 hdmap10.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmap10.l 
 |-  L = ( LSpan ` C )
7 hdmap10.m 
 |-  M = ( ( mapd ` K ) ` W )
8 hdmap10.s 
 |-  S = ( ( HDMap ` K ) ` W )
9 hdmap10.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 hdmap10.t 
 |-  ( ph -> T e. V )
11 sneq 
 |-  ( T = ( 0g ` U ) -> { T } = { ( 0g ` U ) } )
12 11 fveq2d 
 |-  ( T = ( 0g ` U ) -> ( N ` { T } ) = ( N ` { ( 0g ` U ) } ) )
13 12 fveq2d 
 |-  ( T = ( 0g ` U ) -> ( M ` ( N ` { T } ) ) = ( M ` ( N ` { ( 0g ` U ) } ) ) )
14 fveq2 
 |-  ( T = ( 0g ` U ) -> ( S ` T ) = ( S ` ( 0g ` U ) ) )
15 14 sneqd 
 |-  ( T = ( 0g ` U ) -> { ( S ` T ) } = { ( S ` ( 0g ` U ) ) } )
16 15 fveq2d 
 |-  ( T = ( 0g ` U ) -> ( L ` { ( S ` T ) } ) = ( L ` { ( S ` ( 0g ` U ) ) } ) )
17 13 16 eqeq12d 
 |-  ( T = ( 0g ` U ) -> ( ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) <-> ( M ` ( N ` { ( 0g ` U ) } ) ) = ( L ` { ( S ` ( 0g ` U ) ) } ) ) )
18 9 adantr 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( K e. HL /\ W e. H ) )
19 eqid 
 |-  <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >. = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
20 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
21 eqid 
 |-  ( Base ` C ) = ( Base ` C )
22 eqid 
 |-  ( ( HVMap ` K ) ` W ) = ( ( HVMap ` K ) ` W )
23 eqid 
 |-  ( ( HDMap1 ` K ) ` W ) = ( ( HDMap1 ` K ) ` W )
24 10 anim1i 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( T e. V /\ T =/= ( 0g ` U ) ) )
25 eldifsn 
 |-  ( T e. ( V \ { ( 0g ` U ) } ) <-> ( T e. V /\ T =/= ( 0g ` U ) ) )
26 24 25 sylibr 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> T e. ( V \ { ( 0g ` U ) } ) )
27 1 2 3 4 5 6 7 8 18 19 20 21 22 23 26 hdmap10lem 
 |-  ( ( ph /\ T =/= ( 0g ` U ) ) -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )
28 1 2 9 dvhlmod 
 |-  ( ph -> U e. LMod )
29 20 4 lspsn0 
 |-  ( U e. LMod -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
30 28 29 syl 
 |-  ( ph -> ( N ` { ( 0g ` U ) } ) = { ( 0g ` U ) } )
31 30 fveq2d 
 |-  ( ph -> ( M ` ( N ` { ( 0g ` U ) } ) ) = ( M ` { ( 0g ` U ) } ) )
32 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
33 1 7 2 20 5 32 9 mapd0 
 |-  ( ph -> ( M ` { ( 0g ` U ) } ) = { ( 0g ` C ) } )
34 1 2 20 5 32 8 9 hdmapval0 
 |-  ( ph -> ( S ` ( 0g ` U ) ) = ( 0g ` C ) )
35 34 sneqd 
 |-  ( ph -> { ( S ` ( 0g ` U ) ) } = { ( 0g ` C ) } )
36 35 fveq2d 
 |-  ( ph -> ( L ` { ( S ` ( 0g ` U ) ) } ) = ( L ` { ( 0g ` C ) } ) )
37 1 5 9 lcdlmod 
 |-  ( ph -> C e. LMod )
38 32 6 lspsn0 
 |-  ( C e. LMod -> ( L ` { ( 0g ` C ) } ) = { ( 0g ` C ) } )
39 37 38 syl 
 |-  ( ph -> ( L ` { ( 0g ` C ) } ) = { ( 0g ` C ) } )
40 36 39 eqtr2d 
 |-  ( ph -> { ( 0g ` C ) } = ( L ` { ( S ` ( 0g ` U ) ) } ) )
41 31 33 40 3eqtrd 
 |-  ( ph -> ( M ` ( N ` { ( 0g ` U ) } ) ) = ( L ` { ( S ` ( 0g ` U ) ) } ) )
42 17 27 41 pm2.61ne 
 |-  ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )