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 ˙