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	$⊢ \underset{˙}{0} = 0_{U}$
	dvh0g.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
Assertion	dvh0g	$⊢ (K \in HL \land W \in H) \to \underset{˙}{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	$⊢ \underset{˙}{0} = 0_{U}$
6		dvh0g.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
7		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
8	1 2 3	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
9		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
10	1 2 3 9 6	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in 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 \in HL \land W \in H) \land ({I ↾}_{B} \in T \land O \in TEndo (K) (W)) \land ({I ↾}_{B} \in T \land O \in TEndo (K) (W))) \to ⟨{I ↾}_{B}, O⟩ +_{U} ⟨{I ↾}_{B}, O⟩ = ⟨({I ↾}_{B}) \circ ({I ↾}_{B}), O +_{Scalar (U)} O⟩$
15	7 8 10 8 10 14	syl122anc	$⊢ (K \in HL \land W \in H) \to ⟨{I ↾}_{B}, O⟩ +_{U} ⟨{I ↾}_{B}, O⟩ = ⟨({I ↾}_{B}) \circ ({I ↾}_{B}), O +_{Scalar (U)} O⟩$
16		f1oi	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B$
17		f1of	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B \to ({I ↾}_{B}) : B ⟶ B$
18		fcoi2	$⊢ ({I ↾}_{B}) : B ⟶ B \to ({I ↾}_{B}) \circ ({I ↾}_{B}) = {I ↾}_{B}$
19	16 17 18	mp2b	$⊢ ({I ↾}_{B}) \circ ({I ↾}_{B}) = {I ↾}_{B}$
20	19	a1i	$⊢ (K \in HL \land W \in H) \to ({I ↾}_{B}) \circ ({I ↾}_{B}) = {I ↾}_{B}$
21		eqid	$⊢ (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f)))$
22	2 3 9 4 11 21 13	dvhfplusr	$⊢ (K \in HL \land W \in H) \to +_{Scalar (U)} = (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f)))$
23	22	oveqd	$⊢ (K \in HL \land W \in H) \to O +_{Scalar (U)} O = O (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) O$
24	1 2 3 9 6 21	tendo0pl	$⊢ ((K \in HL \land W \in H) \land O \in TEndo (K) (W)) \to O (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) O = O$
25	10 24	mpdan	$⊢ (K \in HL \land W \in H) \to O (s \in TEndo (K) (W), t \in TEndo (K) (W) ⟼ (f \in T ⟼ s (f) \circ t (f))) O = O$
26	23 25	eqtrd	$⊢ (K \in HL \land W \in H) \to O +_{Scalar (U)} O = O$
27	20 26	opeq12d	$⊢ (K \in HL \land W \in H) \to ⟨({I ↾}_{B}) \circ ({I ↾}_{B}), O +_{Scalar (U)} O⟩ = ⟨{I ↾}_{B}, O⟩$
28	15 27	eqtrd	$⊢ (K \in HL \land W \in H) \to ⟨{I ↾}_{B}, O⟩ +_{U} ⟨{I ↾}_{B}, O⟩ = ⟨{I ↾}_{B}, O⟩$
29	2 4 7	dvhlmod	$⊢ (K \in HL \land W \in H) \to U \in LMod$
30		eqid	$⊢ {Base}_{U} = {Base}_{U}$
31	2 3 9 4 30	dvhelvbasei	$⊢ ((K \in HL \land W \in H) \land ({I ↾}_{B} \in T \land O \in TEndo (K) (W))) \to ⟨{I ↾}_{B}, O⟩ \in {Base}_{U}$
32	7 8 10 31	syl12anc	$⊢ (K \in HL \land W \in H) \to ⟨{I ↾}_{B}, O⟩ \in {Base}_{U}$
33	30 12 5	lmod0vid	$⊢ (U \in LMod \land ⟨{I ↾}_{B}, O⟩ \in {Base}_{U}) \to (⟨{I ↾}_{B}, O⟩ +_{U} ⟨{I ↾}_{B}, O⟩ = ⟨{I ↾}_{B}, O⟩ \leftrightarrow \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩)$
34	29 32 33	syl2anc	$⊢ (K \in HL \land W \in H) \to (⟨{I ↾}_{B}, O⟩ +_{U} ⟨{I ↾}_{B}, O⟩ = ⟨{I ↾}_{B}, O⟩ \leftrightarrow \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩)$
35	28 34	mpbid	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} = ⟨{I ↾}_{B}, O⟩$

Metamath Proof Explorer

Theorem dvh0g

Proof