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

Metamath Proof Explorer

Theorem dih0sb

Description: A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses dih0sb.h ⊢ H = LHyp ⁡ K
dih0sb.o ⊢ 0 ˙ = 0. ⁡ K
dih0sb.i ⊢ I = DIsoH ⁡ K ⁡ W
dih0sb.u ⊢ U = DVecH ⁡ K ⁡ W
dih0sb.v ⊢ V = Base U
dih0sb.z ⊢ Z = 0 U
dih0sb.n ⊢ N = LSpan ⁡ U
dih0sb.k ⊢ φ → K ∈ HL ∧ W ∈ H
dih0sb.x ⊢ φ → X ∈ ran ⁡ I
Assertion dih0sb ⊢ φ → X = Z ↔ I -1 ⁡ X = 0 ˙

Proof

Step Hyp Ref Expression
1 dih0sb.h ⊢ H = LHyp ⁡ K
2 dih0sb.o ⊢ 0 ˙ = 0. ⁡ K
3 dih0sb.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dih0sb.u ⊢ U = DVecH ⁡ K ⁡ W
5 dih0sb.v ⊢ V = Base U
6 dih0sb.z ⊢ Z = 0 U
7 dih0sb.n ⊢ N = LSpan ⁡ U
8 dih0sb.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dih0sb.x ⊢ φ → X ∈ ran ⁡ I
10 1 3 4 6 dih0rn ⊢ K ∈ HL ∧ W ∈ H → Z ∈ ran ⁡ I
11 8 10 syl ⊢ φ → Z ∈ ran ⁡ I
12 1 3 8 9 11 dihcnv11 ⊢ φ → I -1 ⁡ X = I -1 ⁡ Z ↔ X = Z
13 1 2 3 4 6 dih0cnv ⊢ K ∈ HL ∧ W ∈ H → I -1 ⁡ Z = 0 ˙
14 8 13 syl ⊢ φ → I -1 ⁡ Z = 0 ˙
15 14 eqeq2d ⊢ φ → I -1 ⁡ X = I -1 ⁡ Z ↔ I -1 ⁡ X = 0 ˙
16 12 15 bitr3d ⊢ φ → X = Z ↔ I -1 ⁡ X = 0 ˙