# Metamath Proof Explorer

## Theorem dvh0g

Description: The zero vector of vector space H has the zero translation as its first member and the zero trace-preserving endomorphism as the second. (Contributed by NM, 9-Mar-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dvh0g.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dvh0g.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvh0g.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dvh0g.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvh0g.z
dvh0g.o ${⊢}{O}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
Assertion dvh0g

### Proof

Step Hyp Ref Expression
1 dvh0g.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dvh0g.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dvh0g.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 dvh0g.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 dvh0g.z
6 dvh0g.o ${⊢}{O}=\left({f}\in {T}⟼{\mathrm{I}↾}_{{B}}\right)$
7 id ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 1 2 3 idltrn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{B}}\in {T}$
9 eqid ${⊢}\mathrm{TEndo}\left({K}\right)\left({W}\right)=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
10 1 2 3 9 6 tendo0cl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)$
11 eqid ${⊢}\mathrm{Scalar}\left({U}\right)=\mathrm{Scalar}\left({U}\right)$
12 eqid ${⊢}{+}_{{U}}={+}_{{U}}$
13 eqid ${⊢}{+}_{\mathrm{Scalar}\left({U}\right)}={+}_{\mathrm{Scalar}\left({U}\right)}$
14 2 3 9 4 11 12 13 dvhopvadd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({\mathrm{I}↾}_{{B}}\in {T}\wedge {O}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)\right)\wedge \left({\mathrm{I}↾}_{{B}}\in {T}\wedge {O}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)\right)\right)\to ⟨{\mathrm{I}↾}_{{B}},{O}⟩{+}_{{U}}⟨{\mathrm{I}↾}_{{B}},{O}⟩=⟨\left({\mathrm{I}↾}_{{B}}\right)\circ \left({\mathrm{I}↾}_{{B}}\right),{O}{+}_{\mathrm{Scalar}\left({U}\right)}{O}⟩$
15 7 8 10 8 10 14 syl122anc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to ⟨{\mathrm{I}↾}_{{B}},{O}⟩{+}_{{U}}⟨{\mathrm{I}↾}_{{B}},{O}⟩=⟨\left({\mathrm{I}↾}_{{B}}\right)\circ \left({\mathrm{I}↾}_{{B}}\right),{O}{+}_{\mathrm{Scalar}\left({U}\right)}{O}⟩$
16 f1oi ${⊢}\left({\mathrm{I}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{B}$
17 f1of ${⊢}\left({\mathrm{I}↾}_{{B}}\right):{B}\underset{1-1 onto}{⟶}{B}\to \left({\mathrm{I}↾}_{{B}}\right):{B}⟶{B}$
18 fcoi2 ${⊢}\left({\mathrm{I}↾}_{{B}}\right):{B}⟶{B}\to \left({\mathrm{I}↾}_{{B}}\right)\circ \left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
19 16 17 18 mp2b ${⊢}\left({\mathrm{I}↾}_{{B}}\right)\circ \left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
20 19 a1i ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \left({\mathrm{I}↾}_{{B}}\right)\circ \left({\mathrm{I}↾}_{{B}}\right)={\mathrm{I}↾}_{{B}}$
21 eqid ${⊢}\left({s}\in \mathrm{TEndo}\left({K}\right)\left({W}\right),{t}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)⟼\left({f}\in {T}⟼{s}\left({f}\right)\circ {t}\left({f}\right)\right)\right)=\left({s}\in \mathrm{TEndo}\left({K}\right)\left({W}\right),{t}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)⟼\left({f}\in {T}⟼{s}\left({f}\right)\circ {t}\left({f}\right)\right)\right)$
22 2 3 9 4 11 21 13 dvhfplusr ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {+}_{\mathrm{Scalar}\left({U}\right)}=\left({s}\in \mathrm{TEndo}\left({K}\right)\left({W}\right),{t}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)⟼\left({f}\in {T}⟼{s}\left({f}\right)\circ {t}\left({f}\right)\right)\right)$
23 22 oveqd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}{+}_{\mathrm{Scalar}\left({U}\right)}{O}={O}\left({s}\in \mathrm{TEndo}\left({K}\right)\left({W}\right),{t}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)⟼\left({f}\in {T}⟼{s}\left({f}\right)\circ {t}\left({f}\right)\right)\right){O}$
24 1 2 3 9 6 21 tendo0pl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {O}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)\right)\to {O}\left({s}\in \mathrm{TEndo}\left({K}\right)\left({W}\right),{t}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)⟼\left({f}\in {T}⟼{s}\left({f}\right)\circ {t}\left({f}\right)\right)\right){O}={O}$
25 10 24 mpdan ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}\left({s}\in \mathrm{TEndo}\left({K}\right)\left({W}\right),{t}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)⟼\left({f}\in {T}⟼{s}\left({f}\right)\circ {t}\left({f}\right)\right)\right){O}={O}$
26 23 25 eqtrd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {O}{+}_{\mathrm{Scalar}\left({U}\right)}{O}={O}$
27 20 26 opeq12d ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to ⟨\left({\mathrm{I}↾}_{{B}}\right)\circ \left({\mathrm{I}↾}_{{B}}\right),{O}{+}_{\mathrm{Scalar}\left({U}\right)}{O}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩$
28 15 27 eqtrd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to ⟨{\mathrm{I}↾}_{{B}},{O}⟩{+}_{{U}}⟨{\mathrm{I}↾}_{{B}},{O}⟩=⟨{\mathrm{I}↾}_{{B}},{O}⟩$
29 2 4 7 dvhlmod ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{LMod}$
30 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
31 2 3 9 4 30 dvhelvbasei ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({\mathrm{I}↾}_{{B}}\in {T}\wedge {O}\in \mathrm{TEndo}\left({K}\right)\left({W}\right)\right)\right)\to ⟨{\mathrm{I}↾}_{{B}},{O}⟩\in {\mathrm{Base}}_{{U}}$
32 7 8 10 31 syl12anc ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to ⟨{\mathrm{I}↾}_{{B}},{O}⟩\in {\mathrm{Base}}_{{U}}$
33 30 12 5 lmod0vid
34 29 32 33 syl2anc
35 28 34 mpbid