Metamath Proof Explorer


Theorem djhj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-Aug-2014)

Ref Expression
Hypotheses djhj.k ˙ = join K
djhj.h H = LHyp K
djhj.i I = DIsoH K W
djhj.j J = joinH K W
djhj.w φ K HL W H
djhj.x φ X ran I
djhj.y φ Y ran I
Assertion djhj φ I -1 X J Y = I -1 X ˙ I -1 Y

Proof

Step Hyp Ref Expression
1 djhj.k ˙ = join K
2 djhj.h H = LHyp K
3 djhj.i I = DIsoH K W
4 djhj.j J = joinH K W
5 djhj.w φ K HL W H
6 djhj.x φ X ran I
7 djhj.y φ Y ran I
8 1 2 3 4 5 6 7 djhjlj φ X J Y = I I -1 X ˙ I -1 Y
9 8 fveq2d φ I -1 X J Y = I -1 I I -1 X ˙ I -1 Y
10 5 simpld φ K HL
11 10 hllatd φ K Lat
12 eqid Base K = Base K
13 12 2 3 dihcnvcl K HL W H X ran I I -1 X Base K
14 5 6 13 syl2anc φ I -1 X Base K
15 12 2 3 dihcnvcl K HL W H Y ran I I -1 Y Base K
16 5 7 15 syl2anc φ I -1 Y Base K
17 12 1 latjcl K Lat I -1 X Base K I -1 Y Base K I -1 X ˙ I -1 Y Base K
18 11 14 16 17 syl3anc φ I -1 X ˙ I -1 Y Base K
19 12 2 3 dihcnvid1 K HL W H I -1 X ˙ I -1 Y Base K I -1 I I -1 X ˙ I -1 Y = I -1 X ˙ I -1 Y
20 5 18 19 syl2anc φ I -1 I I -1 X ˙ I -1 Y = I -1 X ˙ I -1 Y
21 9 20 eqtrd φ I -1 X J Y = I -1 X ˙ I -1 Y