Metamath Proof Explorer


Theorem dihglblem2aN

Description: Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dihglblem.b B = Base K
dihglblem.l ˙ = K
dihglblem.m ˙ = meet K
dihglblem.g G = glb K
dihglblem.h H = LHyp K
dihglblem.t T = u B | v S u = v ˙ W
Assertion dihglblem2aN K HL W H S B S T

Proof

Step Hyp Ref Expression
1 dihglblem.b B = Base K
2 dihglblem.l ˙ = K
3 dihglblem.m ˙ = meet K
4 dihglblem.g G = glb K
5 dihglblem.h H = LHyp K
6 dihglblem.t T = u B | v S u = v ˙ W
7 6 a1i K HL W H S B S T = u B | v S u = v ˙ W
8 simprr K HL W H S B S S
9 n0 S z z S
10 8 9 sylib K HL W H S B S z z S
11 hllat K HL K Lat
12 11 ad3antrrr K HL W H S B S z S K Lat
13 simplrl K HL W H S B S z S S B
14 simpr K HL W H S B S z S z S
15 13 14 sseldd K HL W H S B S z S z B
16 1 5 lhpbase W H W B
17 16 ad3antlr K HL W H S B S z S W B
18 1 3 latmcl K Lat z B W B z ˙ W B
19 12 15 17 18 syl3anc K HL W H S B S z S z ˙ W B
20 eqidd K HL W H S B S z S z ˙ W = z ˙ W
21 oveq1 v = z v ˙ W = z ˙ W
22 21 rspceeqv z S z ˙ W = z ˙ W v S z ˙ W = v ˙ W
23 14 20 22 syl2anc K HL W H S B S z S v S z ˙ W = v ˙ W
24 ovex z ˙ W V
25 eleq1 w = z ˙ W w u B | v S u = v ˙ W z ˙ W u B | v S u = v ˙ W
26 eqeq1 u = z ˙ W u = v ˙ W z ˙ W = v ˙ W
27 26 rexbidv u = z ˙ W v S u = v ˙ W v S z ˙ W = v ˙ W
28 27 elrab z ˙ W u B | v S u = v ˙ W z ˙ W B v S z ˙ W = v ˙ W
29 25 28 bitrdi w = z ˙ W w u B | v S u = v ˙ W z ˙ W B v S z ˙ W = v ˙ W
30 24 29 spcev z ˙ W B v S z ˙ W = v ˙ W w w u B | v S u = v ˙ W
31 19 23 30 syl2anc K HL W H S B S z S w w u B | v S u = v ˙ W
32 n0 u B | v S u = v ˙ W w w u B | v S u = v ˙ W
33 31 32 sylibr K HL W H S B S z S u B | v S u = v ˙ W
34 10 33 exlimddv K HL W H S B S u B | v S u = v ˙ W
35 7 34 eqnetrd K HL W H S B S T