Metamath Proof Explorer


Theorem trlset

Description: The set of traces of lattice translations for a fiducial co-atom W . (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses trlset.b B = Base K
trlset.l ˙ = K
trlset.j ˙ = join K
trlset.m ˙ = meet K
trlset.a A = Atoms K
trlset.h H = LHyp K
trlset.t T = LTrn K W
trlset.r R = trL K W
Assertion trlset K C W H R = f T ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W

Proof

Step Hyp Ref Expression
1 trlset.b B = Base K
2 trlset.l ˙ = K
3 trlset.j ˙ = join K
4 trlset.m ˙ = meet K
5 trlset.a A = Atoms K
6 trlset.h H = LHyp K
7 trlset.t T = LTrn K W
8 trlset.r R = trL K W
9 1 2 3 4 5 6 trlfset K C trL K = w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w
10 9 fveq1d K C trL K W = w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w W
11 8 10 syl5eq K C R = w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w W
12 fveq2 w = W LTrn K w = LTrn K W
13 breq2 w = W p ˙ w p ˙ W
14 13 notbid w = W ¬ p ˙ w ¬ p ˙ W
15 oveq2 w = W p ˙ f p ˙ w = p ˙ f p ˙ W
16 15 eqeq2d w = W x = p ˙ f p ˙ w x = p ˙ f p ˙ W
17 14 16 imbi12d w = W ¬ p ˙ w x = p ˙ f p ˙ w ¬ p ˙ W x = p ˙ f p ˙ W
18 17 ralbidv w = W p A ¬ p ˙ w x = p ˙ f p ˙ w p A ¬ p ˙ W x = p ˙ f p ˙ W
19 18 riotabidv w = W ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w = ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W
20 12 19 mpteq12dv w = W f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w = f LTrn K W ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W
21 eqid w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w = w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w
22 fvex LTrn K W V
23 22 mptex f LTrn K W ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W V
24 20 21 23 fvmpt W H w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w W = f LTrn K W ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W
25 7 mpteq1i f T ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W = f LTrn K W ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W
26 24 25 eqtr4di W H w H f LTrn K w ι x B | p A ¬ p ˙ w x = p ˙ f p ˙ w W = f T ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W
27 11 26 sylan9eq K C W H R = f T ι x B | p A ¬ p ˙ W x = p ˙ f p ˙ W