This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihjatb

Description: Isomorphism H of lattice join of two atoms under the fiducial hyperplane. (Contributed by NM, 23-Sep-2014)

Ref Expression
Hypotheses dihjatb.l ⊢ ≤ ˙ = ≤ K
dihjatb.h ⊢ H = LHyp ⁡ K
dihjatb.j ⊢ ∨ ˙ = join ⁡ K
dihjatb.a ⊢ A = Atoms ⁡ K
dihjatb.u ⊢ U = DVecH ⁡ K ⁡ W
dihjatb.s ⊢ ⊕ ˙ = LSSum ⁡ U
dihjatb.i ⊢ I = DIsoH ⁡ K ⁡ W
dihjatb.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihjatb.p ⊢ φ → P ∈ A ∧ P ≤ ˙ W
dihjatb.q ⊢ φ → Q ∈ A ∧ Q ≤ ˙ W
Assertion dihjatb ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q

Proof

Step Hyp Ref Expression
1 dihjatb.l ⊢ ≤ ˙ = ≤ K
2 dihjatb.h ⊢ H = LHyp ⁡ K
3 dihjatb.j ⊢ ∨ ˙ = join ⁡ K
4 dihjatb.a ⊢ A = Atoms ⁡ K
5 dihjatb.u ⊢ U = DVecH ⁡ K ⁡ W
6 dihjatb.s ⊢ ⊕ ˙ = LSSum ⁡ U
7 dihjatb.i ⊢ I = DIsoH ⁡ K ⁡ W
8 dihjatb.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dihjatb.p ⊢ φ → P ∈ A ∧ P ≤ ˙ W
10 dihjatb.q ⊢ φ → Q ∈ A ∧ Q ≤ ˙ W
11 1 3 4 2 5 6 7 8 9 10 dih2dimb ⊢ φ → I ⁡ P ∨ ˙ Q ⊆ I ⁡ P ⊕ ˙ I ⁡ Q
12 eqid ⊢ Base K = Base K
13 9 simpld ⊢ φ → P ∈ A
14 12 4 atbase ⊢ P ∈ A → P ∈ Base K
15 13 14 syl ⊢ φ → P ∈ Base K
16 10 simpld ⊢ φ → Q ∈ A
17 12 4 atbase ⊢ Q ∈ A → Q ∈ Base K
18 16 17 syl ⊢ φ → Q ∈ Base K
19 12 2 3 5 6 7 8 15 18 dihsumssj ⊢ φ → I ⁡ P ⊕ ˙ I ⁡ Q ⊆ I ⁡ P ∨ ˙ Q
20 11 19 eqssd ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q