Theorem 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	⊢ 0 = ( 0. ‘ 𝐾 )
	dih0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih0.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih0.o	⊢ 𝑂 = ( 0g ‘ 𝑈 )
Assertion	dih0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑂 } )

Proof

Step	Hyp	Ref	Expression
1		dih0.z	⊢ 0 = ( 0. ‘ 𝐾 )
2		dih0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dih0.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dih0.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dih0.o	⊢ 𝑂 = ( 0g ‘ 𝑈 )
6		id	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8	7	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
9		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10	9 1	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
11	8 10	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐾 ) )
12	9 2	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
13		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
14	9 13 1	op0le	⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑊 )
15	7 12 14	syl2an	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ( le ‘ 𝐾 ) 𝑊 )
16		eqid	⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
17	9 13 2 3 16	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 0 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ 0 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) )
18	6 11 15 17	syl12anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) )
19	1 2 16 4 5	dib0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 0 ) = { 𝑂 } )
20	18 19	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑂 } )