Metamath Proof Explorer


Theorem posglbdg

Description: Properties which determine the greatest lower bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses posglbdg.l ˙ = K
posglbdg.b φ B = Base K
posglbdg.g φ G = glb K
posglbdg.k φ K Poset
posglbdg.s φ S B
posglbdg.t φ T B
posglbdg.lb φ x S T ˙ x
posglbdg.gt φ y B x S y ˙ x y ˙ T
Assertion posglbdg φ G S = T

Proof

Step Hyp Ref Expression
1 posglbdg.l ˙ = K
2 posglbdg.b φ B = Base K
3 posglbdg.g φ G = glb K
4 posglbdg.k φ K Poset
5 posglbdg.s φ S B
6 posglbdg.t φ T B
7 posglbdg.lb φ x S T ˙ x
8 posglbdg.gt φ y B x S y ˙ x y ˙ T
9 eqid ODual K = ODual K
10 9 1 oduleval ˙ -1 = ODual K
11 eqid Base K = Base K
12 9 11 odubas Base K = Base ODual K
13 2 12 eqtrdi φ B = Base ODual K
14 eqid glb K = glb K
15 9 14 odulub K Poset glb K = lub ODual K
16 4 15 syl φ glb K = lub ODual K
17 3 16 eqtrd φ G = lub ODual K
18 9 odupos K Poset ODual K Poset
19 4 18 syl φ ODual K Poset
20 vex x V
21 brcnvg x V T B x ˙ -1 T T ˙ x
22 20 6 21 sylancr φ x ˙ -1 T T ˙ x
23 22 adantr φ x S x ˙ -1 T T ˙ x
24 7 23 mpbird φ x S x ˙ -1 T
25 vex y V
26 20 25 brcnv x ˙ -1 y y ˙ x
27 26 ralbii x S x ˙ -1 y x S y ˙ x
28 27 8 syl3an3b φ y B x S x ˙ -1 y y ˙ T
29 brcnvg T B y V T ˙ -1 y y ˙ T
30 6 25 29 sylancl φ T ˙ -1 y y ˙ T
31 30 3ad2ant1 φ y B x S x ˙ -1 y T ˙ -1 y y ˙ T
32 28 31 mpbird φ y B x S x ˙ -1 y T ˙ -1 y
33 10 13 17 19 5 6 24 32 poslubdg φ G S = T