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