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

Metamath Proof Explorer

Theorem dih0bN

Description: A lattice element is zero iff its isomorphism is the zero subspace. (Contributed by NM, 16-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dih0b.b ⊢ B = Base K
dih0b.h ⊢ H = LHyp ⁡ K
dih0b.o ⊢ 0 ˙ = 0. ⁡ K
dih0b.i ⊢ I = DIsoH ⁡ K ⁡ W
dih0b.u ⊢ U = DVecH ⁡ K ⁡ W
dih0b.z ⊢ Z = 0 U
dih0b.k ⊢ φ → K ∈ HL ∧ W ∈ H
dih0b.x ⊢ φ → X ∈ B
Assertion dih0bN ⊢ φ → X = 0 ˙ ↔ I ⁡ X = Z

Proof

Step Hyp Ref Expression
1 dih0b.b ⊢ B = Base K
2 dih0b.h ⊢ H = LHyp ⁡ K
3 dih0b.o ⊢ 0 ˙ = 0. ⁡ K
4 dih0b.i ⊢ I = DIsoH ⁡ K ⁡ W
5 dih0b.u ⊢ U = DVecH ⁡ K ⁡ W
6 dih0b.z ⊢ Z = 0 U
7 dih0b.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dih0b.x ⊢ φ → X ∈ B
9 7 simpld ⊢ φ → K ∈ HL
10 hlop ⊢ K ∈ HL → K ∈ OP
11 1 3 op0cl ⊢ K ∈ OP → 0 ˙ ∈ B
12 9 10 11 3syl ⊢ φ → 0 ˙ ∈ B
13 1 2 4 dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ 0 ˙ ∈ B → I ⁡ X = I ⁡ 0 ˙ ↔ X = 0 ˙
14 7 8 12 13 syl3anc ⊢ φ → I ⁡ X = I ⁡ 0 ˙ ↔ X = 0 ˙
15 3 2 4 5 6 dih0 ⊢ K ∈ HL ∧ W ∈ H → I ⁡ 0 ˙ = Z
16 7 15 syl ⊢ φ → I ⁡ 0 ˙ = Z
17 16 eqeq2d ⊢ φ → I ⁡ X = I ⁡ 0 ˙ ↔ I ⁡ X = Z
18 14 17 bitr3d ⊢ φ → X = 0 ˙ ↔ I ⁡ X = Z