Metamath Proof Explorer

Theorem hdmapeq0

Description: Part of proof of part 12 in Baer p. 49 line 3. (Contributed by NM, 22-May-2015)

Ref Expression
Hypotheses hdmap12a.h 
|- H = ( LHyp ` K )
hdmap12a.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap12a.v 
|- V = ( Base ` U )
hdmap12a.o 
|- .0. = ( 0g ` U )
hdmap12a.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap12a.q 
|- Q = ( 0g ` C )
hdmap12a.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap12a.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap12a.x 
|- ( ph -> T e. V )
Assertion hdmapeq0 
|- ( ph -> ( ( S ` T ) = Q <-> T = .0. ) )

Proof

Step Hyp Ref Expression
1 hdmap12a.h 
 |-  H = ( LHyp ` K )
2 hdmap12a.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap12a.v 
 |-  V = ( Base ` U )
4 hdmap12a.o 
 |-  .0. = ( 0g ` U )
5 hdmap12a.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmap12a.q 
 |-  Q = ( 0g ` C )
7 hdmap12a.s 
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmap12a.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmap12a.x 
 |-  ( ph -> T e. V )
10 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
11 eqid 
 |-  ( LSpan ` C ) = ( LSpan ` C )
12 eqid 
 |-  ( ( mapd ` K ) ` W ) = ( ( mapd ` K ) ` W )
13 1 2 3 10 5 11 12 7 8 9 hdmap10 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { T } ) ) = ( ( LSpan ` C ) ` { ( S ` T ) } ) )
14 1 12 2 4 5 6 8 mapd0 
 |-  ( ph -> ( ( ( mapd ` K ) ` W ) ` { .0. } ) = { Q } )
15 13 14 eqeq12d 
 |-  ( ph -> ( ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { T } ) ) = ( ( ( mapd ` K ) ` W ) ` { .0. } ) <-> ( ( LSpan ` C ) ` { ( S ` T ) } ) = { Q } ) )
16 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
17 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
18 3 16 10 lspsncl 
 |-  ( ( U e. LMod /\ T e. V ) -> ( ( LSpan ` U ) ` { T } ) e. ( LSubSp ` U ) )
19 17 9 18 syl2anc 
 |-  ( ph -> ( ( LSpan ` U ) ` { T } ) e. ( LSubSp ` U ) )
20 4 16 lsssn0 
 |-  ( U e. LMod -> { .0. } e. ( LSubSp ` U ) )
21 17 20 syl 
 |-  ( ph -> { .0. } e. ( LSubSp ` U ) )
22 1 2 16 12 8 19 21 mapd11 
 |-  ( ph -> ( ( ( ( mapd ` K ) ` W ) ` ( ( LSpan ` U ) ` { T } ) ) = ( ( ( mapd ` K ) ` W ) ` { .0. } ) <-> ( ( LSpan ` U ) ` { T } ) = { .0. } ) )
23 1 5 8 lcdlmod 
 |-  ( ph -> C e. LMod )
24 eqid 
 |-  ( Base ` C ) = ( Base ` C )
25 1 2 3 5 24 7 8 9 hdmapcl 
 |-  ( ph -> ( S ` T ) e. ( Base ` C ) )
26 24 6 11 lspsneq0 
 |-  ( ( C e. LMod /\ ( S ` T ) e. ( Base ` C ) ) -> ( ( ( LSpan ` C ) ` { ( S ` T ) } ) = { Q } <-> ( S ` T ) = Q ) )
27 23 25 26 syl2anc 
 |-  ( ph -> ( ( ( LSpan ` C ) ` { ( S ` T ) } ) = { Q } <-> ( S ` T ) = Q ) )
28 15 22 27 3bitr3rd 
 |-  ( ph -> ( ( S ` T ) = Q <-> ( ( LSpan ` U ) ` { T } ) = { .0. } ) )
29 3 4 10 lspsneq0 
 |-  ( ( U e. LMod /\ T e. V ) -> ( ( ( LSpan ` U ) ` { T } ) = { .0. } <-> T = .0. ) )
30 17 9 29 syl2anc 
 |-  ( ph -> ( ( ( LSpan ` U ) ` { T } ) = { .0. } <-> T = .0. ) )
31 28 30 bitrd 
 |-  ( ph -> ( ( S ` T ) = Q <-> T = .0. ) )