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 ˙ = 0 U
Assertion dva0g K HL W 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 ˙ = 0 U
6 id K HL W H K HL W H
7 1 2 3 idltrn K HL W H I B T
8 eqid + U = + U
9 2 3 4 8 dvavadd K HL W H I B T I B T I B + U I B = I B I B
10 6 7 7 9 syl12anc K HL W H I B + U I B = I B 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 I B = I B
14 11 12 13 mp2b I B I B = I B
15 10 14 eqtrdi K HL W H I B + U I B = I B
16 2 4 dvalvec K HL W H U LVec
17 lveclmod U LVec U LMod
18 16 17 syl K HL W H U LMod
19 eqid Base U = Base U
20 2 3 4 19 dvavbase K HL W H Base U = T
21 7 20 eleqtrrd K HL W H I B Base U
22 19 8 5 lmod0vid U LMod I B Base U I B + U I B = I B 0 ˙ = I B
23 18 21 22 syl2anc K HL W H I B + U I B = I B 0 ˙ = I B
24 15 23 mpbid K HL W H 0 ˙ = I B