dih0

Description: The value of isomorphism H at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 9-Mar-2014)

	Ref	Expression
Hypotheses	dih0.z	$⊢ \underset{˙}{0} = 0. (K)$
	dih0.h	$⊢ H = LHyp (K)$
	dih0.i	$⊢ I = DIsoH (K) (W)$
	dih0.u	$⊢ U = DVecH (K) (W)$
	dih0.o	$⊢ O = 0_{U}$
Assertion	dih0	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = \{O\}$

Proof

Step	Hyp	Ref	Expression
1		dih0.z	$⊢ \underset{˙}{0} = 0. (K)$
2		dih0.h	$⊢ H = LHyp (K)$
3		dih0.i	$⊢ I = DIsoH (K) (W)$
4		dih0.u	$⊢ U = DVecH (K) (W)$
5		dih0.o	$⊢ O = 0_{U}$
6		id	$⊢ (K \in HL \land W \in H) \to (K \in HL \land W \in H)$
7		hlop	$⊢ K \in HL \to K \in OP$
8	7	adantr	$⊢ (K \in HL \land W \in H) \to K \in OP$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 1	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
11	8 10	syl	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \in {Base}_{K}$
12	9 2	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
13		eqid	$⊢ \leq_{K} = \leq_{K}$
14	9 13 1	op0le	$⊢ (K \in OP \land W \in {Base}_{K}) \to \underset{˙}{0} \leq_{K} W$
15	7 12 14	syl2an	$⊢ (K \in HL \land W \in H) \to \underset{˙}{0} \leq_{K} W$
16		eqid	$⊢ DIsoB (K) (W) = DIsoB (K) (W)$
17	9 13 2 3 16	dihvalb	$⊢ ((K \in HL \land W \in H) \land (\underset{˙}{0} \in {Base}_{K} \land \underset{˙}{0} \leq_{K} W)) \to I (\underset{˙}{0}) = DIsoB (K) (W) (\underset{˙}{0})$
18	6 11 15 17	syl12anc	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = DIsoB (K) (W) (\underset{˙}{0})$
19	1 2 16 4 5	dib0	$⊢ (K \in HL \land W \in H) \to DIsoB (K) (W) (\underset{˙}{0}) = \{O\}$
20	18 19	eqtrd	$⊢ (K \in HL \land W \in H) \to I (\underset{˙}{0}) = \{O\}$

Metamath Proof Explorer

Theorem dih0

Proof