Metamath Proof Explorer


Theorem dihjat4

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 dihjat4.j ˙ = join K
dihjat4.h H = LHyp K
dihjat4.i I = DIsoH K W
dihjat4.u U = DVecH K W
dihjat4.s ˙ = LSSum U
dihjat4.a A = LSAtoms U
dihjat4.k φ K HL W H
dihjat4.x φ X ran I
dihjat4.q φ Q A
Assertion dihjat4 φ X ˙ Q = I I -1 X ˙ I -1 Q

Proof

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