Metamath Proof Explorer

Theorem dih0

Description: The value of isomorphism H at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 9-Mar-2014)

Ref Expression
Hypotheses dih0.z ⊢ 0 ˙ = 0. ⁡ K
dih0.h ⊢ H = LHyp ⁡ K
dih0.i ⊢ I = DIsoH ⁡ K ⁡ W
dih0.u ⊢ U = DVecH ⁡ K ⁡ W
dih0.o ⊢ O = 0 U
Assertion dih0 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = O

Proof

Step Hyp Ref Expression
1 dih0.z ⊢ 0 ˙ = 0. ⁡ K
2 dih0.h ⊢ H = LHyp ⁡ K
3 dih0.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dih0.u ⊢ U = DVecH ⁡ K ⁡ W
5 dih0.o ⊢ O = 0 U
6 id ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL ∧ W ∈ H
7 hlop ⊢ K ∈ HL → K ∈ OP
8 7 adantr ⊢ K ∈ HL ∧ W ∈ H → K ∈ OP
9 eqid ⊢ Base K = Base K
10 9 1 op0cl ⊢ K ∈ OP → 0 ˙ ∈ Base K
11 8 10 syl ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ Base K
12 9 2 lhpbase ⊢ W ∈ H → W ∈ Base K
13 eqid ⊢ ≤ K = ≤ K
14 9 13 1 op0le ⊢ K ∈ OP ∧ W ∈ Base K → 0 ˙ ≤ K W
15 7 12 14 syl2an ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ≤ K W
16 eqid ⊢ DIsoB ⁡ K ⁡ W = DIsoB ⁡ K ⁡ W
17 9 13 2 3 16 dihvalb ⊢ K ∈ HL ∧ W ∈ H ∧ 0 ˙ ∈ Base K ∧ 0 ˙ ≤ K W → I ⁡ 0 ˙ = DIsoB ⁡ K ⁡ W ⁡ 0 ˙
18 6 11 15 17 syl12anc ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = DIsoB ⁡ K ⁡ W ⁡ 0 ˙
19 1 2 16 4 5 dib0 ⊢ K ∈ HL ∧ W ∈ H → DIsoB ⁡ K ⁡ W ⁡ 0 ˙ = O
20 18 19 eqtrd ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = O