Theorem dih0rn

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

	Ref	Expression
Hypotheses	dih0rn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih0rn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih0rn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih0rn.o	⊢ 0 = ( 0g ‘ 𝑈 )
Assertion	dih0rn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 0 } ∈ ran 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		dih0rn.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dih0rn.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3		dih0rn.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dih0rn.o	⊢ 0 = ( 0g ‘ 𝑈 )
5		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6	5 1 2 3 4	dih0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) = { 0 } )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8	7 1 2	dihfn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn ( Base ‘ 𝐾 ) )
9		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
10	9	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
11	7 5	op0cl	⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
12	10 11	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
13		fnfvelrn	⊢ ( ( 𝐼 Fn ( Base ‘ 𝐾 ) ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ∈ ran 𝐼 )
14	8 12 13	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ ( 0. ‘ 𝐾 ) ) ∈ ran 𝐼 )
15	6 14	eqeltrrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 0 } ∈ ran 𝐼 )