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 = ( 0_g ‘ 𝑈 )
	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 = ( 0_g ‘ 𝑈 )
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 ↾ 𝐵 ) , 𝑂 ⟩ )

Metamath Proof Explorer

Theorem dvh0g

Proof