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