Theorem dih1cnv

Description: The isomorphism H converse value of the full vector space is the lattice one. (Contributed by NM, 19-Jun-2014)

	Ref	Expression
Hypotheses	dih1cnv.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih1cnv.m	⊢ 1 = ( 1. ‘ 𝐾 )
	dih1cnv.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih1cnv.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih1cnv.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
Assertion	dih1cnv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ 𝑉 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		dih1cnv.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dih1cnv.m	⊢ 1 = ( 1. ‘ 𝐾 )
3		dih1cnv.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4		dih1cnv.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		dih1cnv.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6	2 1 3 4 5	dih1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 ‘ 1 ) = 𝑉 )
7	6	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 1 ) ) = ( ◡ 𝐼 ‘ 𝑉 ) )
8		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9	8	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11	10 2	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
12	9 11	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 1 ∈ ( Base ‘ 𝐾 ) )
13	10 1 3	dihcnvid1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 1 ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 1 ) ) = 1 )
14	12 13	mpdan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ 1 ) ) = 1 )
15	7 14	eqtr3d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ 𝑉 ) = 1 )