Metamath Proof Explorer


Theorem dihjat6

Description: Transfer the subspace sum of a closed subspace and an atom back to lattice join. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dihjat6.j ˙ = join K
dihjat6.h H = LHyp K
dihjat6.i I = DIsoH K W
dihjat6.u U = DVecH K W
dihjat6.s ˙ = LSSum U
dihjat6.a A = LSAtoms U
dihjat6.k φ K HL W H
dihjat6.x φ X ran I
dihjat6.q φ Q A
Assertion dihjat6 φ I -1 X ˙ Q = I -1 X ˙ I -1 Q

Proof

Step Hyp Ref Expression
1 dihjat6.j ˙ = join K
2 dihjat6.h H = LHyp K
3 dihjat6.i I = DIsoH K W
4 dihjat6.u U = DVecH K W
5 dihjat6.s ˙ = LSSum U
6 dihjat6.a A = LSAtoms U
7 dihjat6.k φ K HL W H
8 dihjat6.x φ X ran I
9 dihjat6.q φ Q A
10 1 2 3 4 5 6 7 8 9 dihjat4 φ X ˙ Q = I I -1 X ˙ I -1 Q
11 10 fveq2d φ I -1 X ˙ Q = I -1 I I -1 X ˙ I -1 Q
12 7 simpld φ K HL
13 12 hllatd φ K Lat
14 eqid Base K = Base K
15 14 2 3 dihcnvcl K HL W H X ran I I -1 X Base K
16 7 8 15 syl2anc φ I -1 X Base K
17 2 4 3 6 dih1dimat K HL W H Q A Q ran I
18 7 9 17 syl2anc φ Q ran I
19 14 2 3 dihcnvcl K HL W H Q ran I I -1 Q Base K
20 7 18 19 syl2anc φ I -1 Q Base K
21 14 1 latjcl K Lat I -1 X Base K I -1 Q Base K I -1 X ˙ I -1 Q Base K
22 13 16 20 21 syl3anc φ I -1 X ˙ I -1 Q Base K
23 14 2 3 dihcnvid1 K HL W H I -1 X ˙ I -1 Q Base K I -1 I I -1 X ˙ I -1 Q = I -1 X ˙ I -1 Q
24 7 22 23 syl2anc φ I -1 I I -1 X ˙ I -1 Q = I -1 X ˙ I -1 Q
25 11 24 eqtrd φ I -1 X ˙ Q = I -1 X ˙ I -1 Q