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