Metamath Proof Explorer


Theorem dihmeetbN

Description: Isomorphism H of a lattice meet when one element is under the fiducial hyperplane W . (Contributed by NM, 26-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihmeetc.b B = Base K
dihmeetc.l ˙ = K
dihmeetc.m ˙ = meet K
dihmeetc.h H = LHyp K
dihmeetc.i I = DIsoH K W
Assertion dihmeetbN K HL W H X B Y B Y ˙ W I X ˙ Y = I X I Y

Proof

Step Hyp Ref Expression
1 dihmeetc.b B = Base K
2 dihmeetc.l ˙ = K
3 dihmeetc.m ˙ = meet K
4 dihmeetc.h H = LHyp K
5 dihmeetc.i I = DIsoH K W
6 simpl1 K HL W H X B Y B Y ˙ W X ˙ W K HL W H
7 simpl2 K HL W H X B Y B Y ˙ W X ˙ W X B
8 simpr K HL W H X B Y B Y ˙ W X ˙ W X ˙ W
9 simpl3 K HL W H X B Y B Y ˙ W X ˙ W Y B Y ˙ W
10 eqid join K = join K
11 eqid Atoms K = Atoms K
12 eqid oc K W = oc K W
13 eqid LTrn K W = LTrn K W
14 eqid trL K W = trL K W
15 eqid TEndo K W = TEndo K W
16 eqid ι g LTrn K W | g oc K W = q = ι g LTrn K W | g oc K W = q
17 eqid g LTrn K W I B = g LTrn K W I B
18 1 3 4 5 2 10 11 12 13 14 15 16 17 dihmeetlem2N K HL W H X B X ˙ W Y B Y ˙ W I X ˙ Y = I X I Y
19 6 7 8 9 18 syl121anc K HL W H X B Y B Y ˙ W X ˙ W I X ˙ Y = I X I Y
20 simpl1 K HL W H X B Y B Y ˙ W ¬ X ˙ W K HL W H
21 simpl2 K HL W H X B Y B Y ˙ W ¬ X ˙ W X B
22 simpr K HL W H X B Y B Y ˙ W ¬ X ˙ W ¬ X ˙ W
23 simpl3 K HL W H X B Y B Y ˙ W ¬ X ˙ W Y B Y ˙ W
24 1 3 4 5 2 10 11 12 13 14 15 16 17 dihmeetlem1N K HL W H X B ¬ X ˙ W Y B Y ˙ W I X ˙ Y = I X I Y
25 20 21 22 23 24 syl121anc K HL W H X B Y B Y ˙ W ¬ X ˙ W I X ˙ Y = I X I Y
26 19 25 pm2.61dan K HL W H X B Y B Y ˙ W I X ˙ Y = I X I Y