Metamath Proof Explorer


Theorem dihglblem5

Description: Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014)

Ref Expression
Hypotheses dihglblem5.b B = Base K
dihglblem5.g G = glb K
dihglblem5.h H = LHyp K
dihglblem5.u U = DVecH K W
dihglblem5.i I = DIsoH K W
dihglblem5.s S = LSubSp U
Assertion dihglblem5 K HL W H T B T x T I x S

Proof

Step Hyp Ref Expression
1 dihglblem5.b B = Base K
2 dihglblem5.g G = glb K
3 dihglblem5.h H = LHyp K
4 dihglblem5.u U = DVecH K W
5 dihglblem5.i I = DIsoH K W
6 dihglblem5.s S = LSubSp U
7 fvex I x V
8 7 dfiin2 x T I x = y | x T y = I x
9 simpl K HL W H T B T K HL W H
10 3 4 9 dvhlmod K HL W H T B T U LMod
11 simpll K HL W H T B T x T K HL W H
12 simplrl K HL W H T B T x T T B
13 simpr K HL W H T B T x T x T
14 12 13 sseldd K HL W H T B T x T x B
15 1 3 5 4 6 dihlss K HL W H x B I x S
16 11 14 15 syl2anc K HL W H T B T x T I x S
17 16 ralrimiva K HL W H T B T x T I x S
18 uniiunlem x T I x S x T I x S y | x T y = I x S
19 17 18 syl K HL W H T B T x T I x S y | x T y = I x S
20 17 19 mpbid K HL W H T B T y | x T y = I x S
21 simprr K HL W H T B T T
22 n0 T x x T
23 21 22 sylib K HL W H T B T x x T
24 nfre1 x x T y = I x
25 24 nfab _ x y | x T y = I x
26 nfcv _ x
27 25 26 nfne x y | x T y = I x
28 7 elabrex x T I x y | x T y = I x
29 28 ne0d x T y | x T y = I x
30 27 29 exlimi x x T y | x T y = I x
31 23 30 syl K HL W H T B T y | x T y = I x
32 6 lssintcl U LMod y | x T y = I x S y | x T y = I x y | x T y = I x S
33 10 20 31 32 syl3anc K HL W H T B T y | x T y = I x S
34 8 33 eqeltrid K HL W H T B T x T I x S