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