Metamath Proof Explorer

Theorem dihjatcc

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

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

Proof

Step Hyp Ref Expression
1 dihjatcc.l ⊢ ≤ ˙ = ≤ K
2 dihjatcc.h ⊢ H = LHyp ⁡ K
3 dihjatcc.j ⊢ ∨ ˙ = join ⁡ K
4 dihjatcc.a ⊢ A = Atoms ⁡ K
5 dihjatcc.u ⊢ U = DVecH ⁡ K ⁡ W
6 dihjatcc.s ⊢ ⊕ ˙ = LSSum ⁡ U
7 dihjatcc.i ⊢ I = DIsoH ⁡ K ⁡ W
8 dihjatcc.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 dihjatcc.p ⊢ φ → P ∈ A ∧ ¬ P ≤ ˙ W
10 dihjatcc.q ⊢ φ → Q ∈ A ∧ ¬ Q ≤ ˙ W
11 eqid ⊢ Base K = Base K
12 eqid ⊢ meet ⁡ K = meet ⁡ K
13 eqid ⊢ P ∨ ˙ Q meet ⁡ K W = P ∨ ˙ Q meet ⁡ K W
14 eqid ⊢ oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
15 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
16 eqid ⊢ trL ⁡ K ⁡ W = trL ⁡ K ⁡ W
17 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
18 eqid ⊢ ι d ∈ LTrn ⁡ K ⁡ W | d ⁡ oc ⁡ K ⁡ W = P = ι d ∈ LTrn ⁡ K ⁡ W | d ⁡ oc ⁡ K ⁡ W = P
19 eqid ⊢ ι d ∈ LTrn ⁡ K ⁡ W | d ⁡ oc ⁡ K ⁡ W = Q = ι d ∈ LTrn ⁡ K ⁡ W | d ⁡ oc ⁡ K ⁡ W = Q
20 eqid ⊢ a ∈ TEndo ⁡ K ⁡ W ⟼ d ∈ LTrn ⁡ K ⁡ W ⟼ a ⁡ d -1 = a ∈ TEndo ⁡ K ⁡ W ⟼ d ∈ LTrn ⁡ K ⁡ W ⟼ a ⁡ d -1
21 eqid ⊢ d ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K = d ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ Base K
22 eqid ⊢ a ∈ TEndo ⁡ K ⁡ W , b ∈ TEndo ⁡ K ⁡ W ⟼ d ∈ LTrn ⁡ K ⁡ W ⟼ a ⁡ d ∘ b ⁡ d = a ∈ TEndo ⁡ K ⁡ W , b ∈ TEndo ⁡ K ⁡ W ⟼ d ∈ LTrn ⁡ K ⁡ W ⟼ a ⁡ d ∘ b ⁡ d
23 11 1 2 3 12 4 5 6 7 13 8 9 10 14 15 16 17 18 19 20 21 22 dihjatcclem4 ⊢ φ → I ⁡ P ∨ ˙ Q meet ⁡ K W ⊆ I ⁡ P ⊕ ˙ I ⁡ Q
24 11 1 2 3 12 4 5 6 7 13 8 9 10 23 dihjatcclem2 ⊢ φ → I ⁡ P ∨ ˙ Q = I ⁡ P ⊕ ˙ I ⁡ Q