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 = Base K
dvh0g.h ⊢ H = LHyp ⁡ K
dvh0g.t ⊢ T = LTrn ⁡ K ⁡ W
dvh0g.u ⊢ U = DVecH ⁡ K ⁡ W
dvh0g.z ⊢ 0 ˙ = 0 U
dvh0g.o ⊢ O = f ∈ T ⟼ I ↾ B
Assertion dvh0g ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ = I ↾ B O

Proof

Step Hyp Ref Expression
1 dvh0g.b ⊢ B = Base K
2 dvh0g.h ⊢ H = LHyp ⁡ K
3 dvh0g.t ⊢ T = LTrn ⁡ K ⁡ W
4 dvh0g.u ⊢ U = DVecH ⁡ K ⁡ W
5 dvh0g.z ⊢ 0 ˙ = 0 U
6 dvh0g.o ⊢ O = f ∈ T ⟼ I ↾ B
7 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
8 1 2 3 idltrn ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∈ T
9 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
10 1 2 3 9 6 tendo0cl ⊢ K ∈ HL ∧ W ∈ H → O ∈ TEndo ⁡ K ⁡ W
11 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
12 eqid ⊢ + U = + U
13 eqid ⊢ + Scalar ⁡ U = + Scalar ⁡ U
14 2 3 9 4 11 12 13 dvhopvadd ⊢ K ∈ HL ∧ W ∈ H ∧ I ↾ B ∈ T ∧ O ∈ TEndo ⁡ K ⁡ W ∧ I ↾ B ∈ T ∧ O ∈ TEndo ⁡ K ⁡ W → I ↾ B O + U I ↾ B O = I ↾ B ∘ I ↾ B O + Scalar ⁡ U O
15 7 8 10 8 10 14 syl122anc ⊢ K ∈ HL ∧ W ∈ H → I ↾ B O + U I ↾ B O = I ↾ B ∘ I ↾ B O + Scalar ⁡ U O
16 f1oi ⊢ I ↾ B : B ⟶ 1-1 onto B
17 f1of ⊢ I ↾ B : B ⟶ 1-1 onto B → I ↾ B : B ⟶ B
18 fcoi2 ⊢ I ↾ B : B ⟶ B → I ↾ B ∘ I ↾ B = I ↾ B
19 16 17 18 mp2b ⊢ I ↾ B ∘ I ↾ B = I ↾ B
20 19 a1i ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∘ I ↾ B = I ↾ B
21 eqid ⊢ s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f = s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
22 2 3 9 4 11 21 13 dvhfplusr ⊢ K ∈ HL ∧ W ∈ H → + Scalar ⁡ U = s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f
23 22 oveqd ⊢ K ∈ HL ∧ W ∈ H → O + Scalar ⁡ U O = O s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f O
24 1 2 3 9 6 21 tendo0pl ⊢ K ∈ HL ∧ W ∈ H ∧ O ∈ TEndo ⁡ K ⁡ W → O s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f O = O
25 10 24 mpdan ⊢ K ∈ HL ∧ W ∈ H → O s ∈ TEndo ⁡ K ⁡ W , t ∈ TEndo ⁡ K ⁡ W ⟼ f ∈ T ⟼ s ⁡ f ∘ t ⁡ f O = O
26 23 25 eqtrd ⊢ K ∈ HL ∧ W ∈ H → O + Scalar ⁡ U O = O
27 20 26 opeq12d ⊢ K ∈ HL ∧ W ∈ H → I ↾ B ∘ I ↾ B O + Scalar ⁡ U O = I ↾ B O
28 15 27 eqtrd ⊢ K ∈ HL ∧ W ∈ H → I ↾ B O + U I ↾ B O = I ↾ B O
29 2 4 7 dvhlmod ⊢ K ∈ HL ∧ W ∈ H → U ∈ LMod
30 eqid ⊢ Base U = Base U
31 2 3 9 4 30 dvhelvbasei ⊢ K ∈ HL ∧ W ∈ H ∧ I ↾ B ∈ T ∧ O ∈ TEndo ⁡ K ⁡ W → I ↾ B O ∈ Base U
32 7 8 10 31 syl12anc ⊢ K ∈ HL ∧ W ∈ H → I ↾ B O ∈ Base U
33 30 12 5 lmod0vid ⊢ U ∈ LMod ∧ I ↾ B O ∈ Base U → I ↾ B O + U I ↾ B O = I ↾ B O ↔ 0 ˙ = I ↾ B O
34 29 32 33 syl2anc ⊢ K ∈ HL ∧ W ∈ H → I ↾ B O + U I ↾ B O = I ↾ B O ↔ 0 ˙ = I ↾ B O
35 28 34 mpbid ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ = I ↾ B O