Metamath Proof Explorer

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 ⊢ H = LHyp ⁡ K
dih0cnv.o ⊢ 0 ˙ = 0. ⁡ K
dih0cnv.i ⊢ I = DIsoH ⁡ K ⁡ W
dih0cnv.u ⊢ U = DVecH ⁡ K ⁡ W
dih0cnv.z ⊢ Z = 0 U
Assertion dih0cnv ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ Z = 0 ˙

Proof

Step Hyp Ref Expression
1 dih0cnv.h ⊢ H = LHyp ⁡ K
2 dih0cnv.o ⊢ 0 ˙ = 0. ⁡ K
3 dih0cnv.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dih0cnv.u ⊢ U = DVecH ⁡ K ⁡ W
5 dih0cnv.z ⊢ Z = 0 U
6 2 1 3 4 5 dih0 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = Z
7 6 fveq2d ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ I ⁡ 0 ˙ = I -1 ⁡ Z
8 hlatl ⊢ K ∈ HL → K ∈ AtLat
9 8 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ AtLat
10 eqid ⊢ Base K = Base K
11 10 2 atl0cl ⊢ K ∈ AtLat → 0 ˙ ∈ Base K
12 9 11 syl ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ Base K
13 10 1 3 dihcnvid1 ⊢ K ∈ HL ∧ W ∈ H ∧ 0 ˙ ∈ Base K → I -1 ⁡ I ⁡ 0 ˙ = 0 ˙
14 12 13 mpdan ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ I ⁡ 0 ˙ = 0 ˙
15 7 14 eqtr3d ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ Z = 0 ˙