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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
dvh0g.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh0g.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvh0g.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh0g.z ⊢ 0 = ( 0g ‘ 𝑈 )
dvh0g.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
Assertion dvh0g ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )

Proof

Step Hyp Ref Expression
1 dvh0g.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dvh0g.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dvh0g.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 dvh0g.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvh0g.z ⊢ 0 = ( 0g ‘ 𝑈 )
6 dvh0g.o ⊢ 𝑂 = ( 𝑓 ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
7 id ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 1 2 3 idltrn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
9 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
10 1 2 3 9 6 tendo0cl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
11 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
12 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
13 eqid ⊢ ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( +g ‘ ( Scalar ‘ 𝑈 ) )
14 2 3 9 4 11 12 13 dvhopvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) = ⟨ ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ )
15 7 8 10 8 10 14 syl122anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) = ⟨ ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ )
16 f1oi ⊢ ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵
17 f1of ⊢ ( ( I ↾ 𝐵 ) : 𝐵 –1-1-onto→ 𝐵 → ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 )
18 fcoi2 ⊢ ( ( I ↾ 𝐵 ) : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
19 16 17 18 mp2b ⊢ ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 )
20 19 a1i ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) = ( I ↾ 𝐵 ) )
21 eqid ⊢ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) )
22 2 3 9 4 11 21 13 dvhfplusr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( +g ‘ ( Scalar ‘ 𝑈 ) ) = ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) )
23 22 oveqd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) = ( 𝑂 ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) 𝑂 ) )
24 1 2 3 9 6 21 tendo0pl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑂 ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) 𝑂 ) = 𝑂 )
25 10 24 mpdan ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) , 𝑡 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( 𝑓 ∈ 𝑇 ↦ ( ( 𝑠 ‘ 𝑓 ) ∘ ( 𝑡 ‘ 𝑓 ) ) ) ) 𝑂 ) = 𝑂 )
26 23 25 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) = 𝑂 )
27 20 26 opeq12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⟨ ( ( I ↾ 𝐵 ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑂 ( +g ‘ ( Scalar ‘ 𝑈 ) ) 𝑂 ) ⟩ = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
28 15 27 eqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )
29 2 4 7 dvhlmod ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LMod )
30 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
31 2 3 9 4 30 dvhelvbasei ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) )
32 7 8 10 31 syl12anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) )
33 30 12 5 lmod0vid ⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) ) → ( ( ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ↔ 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) )
34 29 32 33 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ( +g ‘ 𝑈 ) ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ↔ 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ ) )
35 28 34 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 = ⟨ ( I ↾ 𝐵 ) , 𝑂 ⟩ )