Metamath Proof Explorer


Theorem dihglblem5aN

Description: A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem5a.b B = Base K
dihglblem5a.m ˙ = meet K
dihglblem5a.h H = LHyp K
dihglblem5a.i I = DIsoH K W
Assertion dihglblem5aN K HL W H X B I X ˙ W = I X I W

Proof

Step Hyp Ref Expression
1 dihglblem5a.b B = Base K
2 dihglblem5a.m ˙ = meet K
3 dihglblem5a.h H = LHyp K
4 dihglblem5a.i I = DIsoH K W
5 simpr K HL W H X B X K W X K W
6 hllat K HL K Lat
7 6 ad3antrrr K HL W H X B X K W K Lat
8 simplr K HL W H X B X K W X B
9 1 3 lhpbase W H W B
10 9 ad3antlr K HL W H X B X K W W B
11 eqid K = K
12 1 11 2 latleeqm1 K Lat X B W B X K W X ˙ W = X
13 7 8 10 12 syl3anc K HL W H X B X K W X K W X ˙ W = X
14 5 13 mpbid K HL W H X B X K W X ˙ W = X
15 14 fveq2d K HL W H X B X K W I X ˙ W = I X
16 simpll K HL W H X B X K W K HL W H
17 1 11 3 4 dihord K HL W H X B W B I X I W X K W
18 16 8 10 17 syl3anc K HL W H X B X K W I X I W X K W
19 5 18 mpbird K HL W H X B X K W I X I W
20 df-ss I X I W I X I W = I X
21 19 20 sylib K HL W H X B X K W I X I W = I X
22 15 21 eqtr4d K HL W H X B X K W I X ˙ W = I X I W
23 eqid join K = join K
24 eqid Atoms K = Atoms K
25 eqid oc K W = oc K W
26 eqid LTrn K W = LTrn K W
27 eqid trL K W = trL K W
28 eqid TEndo K W = TEndo K W
29 eqid ι h LTrn K W | h oc K W = q = ι h LTrn K W | h oc K W = q
30 eqid h LTrn K W I B = h LTrn K W I B
31 1 2 3 4 11 23 24 25 26 27 28 29 30 dihglblem5apreN K HL W H X B ¬ X K W I X ˙ W = I X I W
32 31 anassrs K HL W H X B ¬ X K W I X ˙ W = I X I W
33 22 32 pm2.61dan K HL W H X B I X ˙ W = I X I W