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 ⊢BaseK=BaseK
12 eqid ⊢meet⁡K=meet⁡K
13 eqid ⊢P∨˙Qmeet⁡KW=P∨˙Qmeet⁡KW
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↾BaseK=d∈LTrn⁡K⁡W⟼I↾BaseK
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∨˙Qmeet⁡KW⊆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