This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )