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=BaseK
dva0g.h ⊢H=LHyp⁡K
dva0g.t ⊢T=LTrn⁡K⁡W
dva0g.u ⊢U=DVecA⁡K⁡W
dva0g.z ⊢0˙=0U
Assertion dva0g ⊢K∈HL∧W∈H→0˙=I↾B

Proof

Step Hyp Ref Expression
1 dva0g.b ⊢B=BaseK
2 dva0g.h ⊢H=LHyp⁡K
3 dva0g.t ⊢T=LTrn⁡K⁡W
4 dva0g.u ⊢U=DVecA⁡K⁡W
5 dva0g.z ⊢0˙=0U
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+UI↾B=I↾B∘I↾B
10 6 7 7 9 syl12anc ⊢K∈HL∧W∈H→I↾B+UI↾B=I↾B∘I↾B
11 f1oi ⊢I↾B:B⟶1-1 ontoB
12 f1of ⊢I↾B:B⟶1-1 ontoB→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+UI↾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 ⊢BaseU=BaseU
20 2 3 4 19 dvavbase ⊢K∈HL∧W∈H→BaseU=T
21 7 20 eleqtrrd ⊢K∈HL∧W∈H→I↾B∈BaseU
22 19 8 5 lmod0vid ⊢U∈LMod∧I↾B∈BaseU→I↾B+UI↾B=I↾B↔0˙=I↾B
23 18 21 22 syl2anc ⊢K∈HL∧W∈H→I↾B+UI↾B=I↾B↔0˙=I↾B
24 15 23 mpbid ⊢K∈HL∧W∈H→0˙=I↾B