Metamath Proof Explorer

Theorem dva0g

Description: The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014)

Ref Expression
Hypotheses dva0g.b 
|- B = ( Base ` K )
dva0g.h 
|- H = ( LHyp ` K )
dva0g.t 
|- T = ( ( LTrn ` K ) ` W )
dva0g.u 
|- U = ( ( DVecA ` K ) ` W )
dva0g.z 
|- .0. = ( 0g ` U )
Assertion dva0g 
|- ( ( K e. HL /\ W e. H ) -> .0. = ( _I |` B ) )

Proof

Step Hyp Ref Expression
1 dva0g.b 
 |-  B = ( Base ` K )
2 dva0g.h 
 |-  H = ( LHyp ` K )
3 dva0g.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 dva0g.u 
 |-  U = ( ( DVecA ` K ) ` W )
5 dva0g.z 
 |-  .0. = ( 0g ` U )
6 id 
 |-  ( ( K e. HL /\ W e. H ) -> ( K e. HL /\ W e. H ) )
7 1 2 3 idltrn 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )
8 eqid 
 |-  ( +g ` U ) = ( +g ` U )
9 2 3 4 8 dvavadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( _I |` B ) e. T /\ ( _I |` B ) e. T ) ) -> ( ( _I |` B ) ( +g ` U ) ( _I |` B ) ) = ( ( _I |` B ) o. ( _I |` B ) ) )
10 6 7 7 9 syl12anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` B ) ( +g ` U ) ( _I |` B ) ) = ( ( _I |` B ) o. ( _I |` B ) ) )
11 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
12 f1of 
 |-  ( ( _I |` B ) : B -1-1-onto-> B -> ( _I |` B ) : B --> B )
13 fcoi2 
 |-  ( ( _I |` B ) : B --> B -> ( ( _I |` B ) o. ( _I |` B ) ) = ( _I |` B ) )
14 11 12 13 mp2b 
 |-  ( ( _I |` B ) o. ( _I |` B ) ) = ( _I |` B )
15 10 14 eqtrdi 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` B ) ( +g ` U ) ( _I |` B ) ) = ( _I |` B ) )
16 2 4 dvalvec 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LVec )
17 lveclmod 
 |-  ( U e. LVec -> U e. LMod )
18 16 17 syl 
 |-  ( ( K e. HL /\ W e. H ) -> U e. LMod )
19 eqid 
 |-  ( Base ` U ) = ( Base ` U )
20 2 3 4 19 dvavbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` U ) = T )
21 7 20 eleqtrrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. ( Base ` U ) )
22 19 8 5 lmod0vid 
 |-  ( ( U e. LMod /\ ( _I |` B ) e. ( Base ` U ) ) -> ( ( ( _I |` B ) ( +g ` U ) ( _I |` B ) ) = ( _I |` B ) <-> .0. = ( _I |` B ) ) )
23 18 21 22 syl2anc 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( _I |` B ) ( +g ` U ) ( _I |` B ) ) = ( _I |` B ) <-> .0. = ( _I |` B ) ) )
24 15 23 mpbid 
 |-  ( ( K e. HL /\ W e. H ) -> .0. = ( _I |` B ) )