Metamath Proof Explorer


Theorem djh02

Description: Closed subspace join with zero. (Contributed by NM, 9-Aug-2014)

Ref Expression
Hypotheses djh01.h H = LHyp K
djh01.u U = DVecH K W
djh01.o 0 ˙ = 0 U
djh01.i I = DIsoH K W
djh01.j ˙ = joinH K W
djh01.k φ K HL W H
djh01.x φ X ran I
Assertion djh02 φ 0 ˙ ˙ X = X

Proof

Step Hyp Ref Expression
1 djh01.h H = LHyp K
2 djh01.u U = DVecH K W
3 djh01.o 0 ˙ = 0 U
4 djh01.i I = DIsoH K W
5 djh01.j ˙ = joinH K W
6 djh01.k φ K HL W H
7 djh01.x φ X ran I
8 eqid Base U = Base U
9 1 4 2 3 dih0rn K HL W H 0 ˙ ran I
10 1 2 4 8 dihrnss K HL W H 0 ˙ ran I 0 ˙ Base U
11 6 9 10 syl2anc2 φ 0 ˙ Base U
12 1 2 4 8 dihrnss K HL W H X ran I X Base U
13 6 7 12 syl2anc φ X Base U
14 1 2 8 5 6 11 13 djhcom φ 0 ˙ ˙ X = X ˙ 0 ˙
15 1 2 3 4 5 6 7 djh01 φ X ˙ 0 ˙ = X
16 14 15 eqtrd φ 0 ˙ ˙ X = X