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 ⊢ H = LHyp ⁡ K
dih1cnv.m ⊢ 1 ˙ = 1. ⁡ K
dih1cnv.i ⊢ I = DIsoH ⁡ K ⁡ W
dih1cnv.u ⊢ U = DVecH ⁡ K ⁡ W
dih1cnv.v ⊢ V = Base U
Assertion dih1cnv ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ V = 1 ˙

Proof

Step Hyp Ref Expression
1 dih1cnv.h ⊢ H = LHyp ⁡ K
2 dih1cnv.m ⊢ 1 ˙ = 1. ⁡ K
3 dih1cnv.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dih1cnv.u ⊢ U = DVecH ⁡ K ⁡ W
5 dih1cnv.v ⊢ V = Base U
6 2 1 3 4 5 dih1 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 1 ˙ = V
7 6 fveq2d ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ I ⁡ 1 ˙ = I -1 ⁡ V
8 hlop ⊢ K ∈ HL → K ∈ OP
9 8 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ OP
10 eqid ⊢ Base K = Base K
11 10 2 op1cl ⊢ K ∈ OP → 1 ˙ ∈ Base K
12 9 11 syl ⊢ K ∈ HL ∧ W ∈ H → 1 ˙ ∈ Base K
13 10 1 3 dihcnvid1 ⊢ K ∈ HL ∧ W ∈ H ∧ 1 ˙ ∈ Base K → I -1 ⁡ I ⁡ 1 ˙ = 1 ˙
14 12 13 mpdan ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ I ⁡ 1 ˙ = 1 ˙
15 7 14 eqtr3d ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ V = 1 ˙