Metamath Proof Explorer


Theorem djh01

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 djh01 φ X ˙ 0 ˙ = 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 join K = join K
9 1 4 2 3 dih0rn K HL W H 0 ˙ ran I
10 6 9 syl φ 0 ˙ ran I
11 8 1 4 5 6 7 10 djhjlj φ X ˙ 0 ˙ = I I -1 X join K I -1 0 ˙
12 eqid 0. K = 0. K
13 1 12 4 2 3 dih0cnv K HL W H I -1 0 ˙ = 0. K
14 6 13 syl φ I -1 0 ˙ = 0. K
15 14 oveq2d φ I -1 X join K I -1 0 ˙ = I -1 X join K 0. K
16 6 simpld φ K HL
17 hlol K HL K OL
18 16 17 syl φ K OL
19 eqid Base K = Base K
20 19 1 4 dihcnvcl K HL W H X ran I I -1 X Base K
21 6 7 20 syl2anc φ I -1 X Base K
22 19 8 12 olj01 K OL I -1 X Base K I -1 X join K 0. K = I -1 X
23 18 21 22 syl2anc φ I -1 X join K 0. K = I -1 X
24 15 23 eqtrd φ I -1 X join K I -1 0 ˙ = I -1 X
25 24 fveq2d φ I I -1 X join K I -1 0 ˙ = I I -1 X
26 1 4 dihcnvid2 K HL W H X ran I I I -1 X = X
27 6 7 26 syl2anc φ I I -1 X = X
28 11 25 27 3eqtrd φ X ˙ 0 ˙ = X