Metamath Proof Explorer


Theorem diaglbN

Description: Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses diaglb.g G = glb K
diaglb.h H = LHyp K
diaglb.i I = DIsoA K W
Assertion diaglbN K HL W H S dom I S I G S = x S I x

Proof

Step Hyp Ref Expression
1 diaglb.g G = glb K
2 diaglb.h H = LHyp K
3 diaglb.i I = DIsoA K W
4 simpl K HL W H S dom I S K HL W H
5 hlclat K HL K CLat
6 5 ad2antrr K HL W H S dom I S K CLat
7 eqid Base K = Base K
8 eqid K = K
9 7 8 2 3 diadm K HL W H dom I = y Base K | y K W
10 9 sseq2d K HL W H S dom I S y Base K | y K W
11 10 biimpa K HL W H S dom I S y Base K | y K W
12 11 adantrr K HL W H S dom I S S y Base K | y K W
13 ssrab2 y Base K | y K W Base K
14 12 13 sstrdi K HL W H S dom I S S Base K
15 7 1 clatglbcl K CLat S Base K G S Base K
16 6 14 15 syl2anc K HL W H S dom I S G S Base K
17 simprr K HL W H S dom I S S
18 n0 S x x S
19 17 18 sylib K HL W H S dom I S x x S
20 hllat K HL K Lat
21 20 ad3antrrr K HL W H S dom I S x S K Lat
22 16 adantr K HL W H S dom I S x S G S Base K
23 ssel2 S dom I x S x dom I
24 23 adantlr S dom I S x S x dom I
25 24 adantll K HL W H S dom I S x S x dom I
26 7 8 2 3 diaeldm K HL W H x dom I x Base K x K W
27 26 ad2antrr K HL W H S dom I S x S x dom I x Base K x K W
28 25 27 mpbid K HL W H S dom I S x S x Base K x K W
29 28 simpld K HL W H S dom I S x S x Base K
30 7 2 lhpbase W H W Base K
31 30 ad3antlr K HL W H S dom I S x S W Base K
32 5 ad3antrrr K HL W H S dom I S x S K CLat
33 14 adantr K HL W H S dom I S x S S Base K
34 simpr K HL W H S dom I S x S x S
35 7 8 1 clatglble K CLat S Base K x S G S K x
36 32 33 34 35 syl3anc K HL W H S dom I S x S G S K x
37 28 simprd K HL W H S dom I S x S x K W
38 7 8 21 22 29 31 36 37 lattrd K HL W H S dom I S x S G S K W
39 19 38 exlimddv K HL W H S dom I S G S K W
40 eqid LTrn K W = LTrn K W
41 eqid trL K W = trL K W
42 7 8 2 40 41 3 diaelval K HL W H G S Base K G S K W f I G S f LTrn K W trL K W f K G S
43 4 16 39 42 syl12anc K HL W H S dom I S f I G S f LTrn K W trL K W f K G S
44 r19.28zv S x S f LTrn K W trL K W f K x f LTrn K W x S trL K W f K x
45 44 ad2antll K HL W H S dom I S x S f LTrn K W trL K W f K x f LTrn K W x S trL K W f K x
46 simpll K HL W H S dom I S x S K HL W H
47 7 8 2 40 41 3 diaelval K HL W H x Base K x K W f I x f LTrn K W trL K W f K x
48 46 28 47 syl2anc K HL W H S dom I S x S f I x f LTrn K W trL K W f K x
49 48 ralbidva K HL W H S dom I S x S f I x x S f LTrn K W trL K W f K x
50 5 ad3antrrr K HL W H S dom I S f LTrn K W K CLat
51 7 2 40 41 trlcl K HL W H f LTrn K W trL K W f Base K
52 51 adantlr K HL W H S dom I S f LTrn K W trL K W f Base K
53 14 adantr K HL W H S dom I S f LTrn K W S Base K
54 7 8 1 clatleglb K CLat trL K W f Base K S Base K trL K W f K G S x S trL K W f K x
55 50 52 53 54 syl3anc K HL W H S dom I S f LTrn K W trL K W f K G S x S trL K W f K x
56 55 pm5.32da K HL W H S dom I S f LTrn K W trL K W f K G S f LTrn K W x S trL K W f K x
57 45 49 56 3bitr4rd K HL W H S dom I S f LTrn K W trL K W f K G S x S f I x
58 vex f V
59 eliin f V f x S I x x S f I x
60 58 59 ax-mp f x S I x x S f I x
61 57 60 bitr4di K HL W H S dom I S f LTrn K W trL K W f K G S f x S I x
62 43 61 bitrd K HL W H S dom I S f I G S f x S I x
63 62 eqrdv K HL W H S dom I S I G S = x S I x