Theorem dih0cnv

Description: The isomorphism H converse value of the zero subspace is the lattice zero. (Contributed by NM, 19-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dih0cnv.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dih0cnv.o	⊢ 0 = ( 0. ‘ 𝐾 )
3		dih0cnv.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dih0cnv.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dih0cnv.z	⊢ 𝑍 = ( 0g ‘ 𝑈 )
6	2 1 3 4 5	dih0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 0 ) = { 𝑍 } )
7	6	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 0 ) ) = ( ◡ 𝐼 ‘ { 𝑍 } ) )
8		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
9	8	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ AtLat )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11	10 2	atl0cl	⊢ ( 𝐾 ∈ AtLat → 0 ∈ ( Base ‘ 𝐾 ) )
12	9 11	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐾 ) )
13	10 1 3	dihcnvid1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 0 ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 0 ) ) = 0 )
14	12 13	mpdan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 0 ) ) = 0 )
15	7 14	eqtr3d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ { 𝑍 } ) = 0 )