dih0rn

Description: The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014)

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

Step	Hyp	Ref	Expression
1		dih0rn.h	$⊢ H = LHyp (K)$
2		dih0rn.i	$⊢ I = DIsoH (K) (W)$
3		dih0rn.u	$⊢ U = DVecH (K) (W)$
4		dih0rn.o	$⊢ \underset{˙}{0} = 0_{U}$
5		eqid	$⊢ 0. (K) = 0. (K)$
6	5 1 2 3 4	dih0	$⊢ (K \in HL \land W \in H) \to I (0. (K)) = \{\underset{˙}{0}\}$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 1 2	dihfn	$⊢ (K \in HL \land W \in H) \to I Fn {Base}_{K}$
9		hlop	$⊢ K \in HL \to K \in OP$
10	9	adantr	$⊢ (K \in HL \land W \in H) \to K \in OP$
11	7 5	op0cl	$⊢ K \in OP \to 0. (K) \in {Base}_{K}$
12	10 11	syl	$⊢ (K \in HL \land W \in H) \to 0. (K) \in {Base}_{K}$
13		fnfvelrn	$⊢ (I Fn {Base}_{K} \land 0. (K) \in {Base}_{K}) \to I (0. (K)) \in ran I$
14	8 12 13	syl2anc	$⊢ (K \in HL \land W \in H) \to I (0. (K)) \in ran I$
15	6 14	eqeltrrd	$⊢ (K \in HL \land W \in H) \to \{\underset{˙}{0}\} \in ran I$

Metamath Proof Explorer