Metamath Proof Explorer


Theorem ltrnset

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

Ref Expression
Hypotheses ltrnset.l ˙ = K
ltrnset.j ˙ = join K
ltrnset.m ˙ = meet K
ltrnset.a A = Atoms K
ltrnset.h H = LHyp K
ltrnset.d D = LDil K W
ltrnset.t T = LTrn K W
Assertion ltrnset K B W H T = f D | p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W

Proof

Step Hyp Ref Expression
1 ltrnset.l ˙ = K
2 ltrnset.j ˙ = join K
3 ltrnset.m ˙ = meet K
4 ltrnset.a A = Atoms K
5 ltrnset.h H = LHyp K
6 ltrnset.d D = LDil K W
7 ltrnset.t T = LTrn K W
8 1 2 3 4 5 ltrnfset K B LTrn K = w H f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w
9 8 fveq1d K B LTrn K W = w H f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w W
10 7 9 syl5eq K B T = w H f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w W
11 fveq2 w = W LDil K w = LDil K W
12 11 6 eqtr4di w = W LDil K w = D
13 breq2 w = W p ˙ w p ˙ W
14 13 notbid w = W ¬ p ˙ w ¬ p ˙ W
15 breq2 w = W q ˙ w q ˙ W
16 15 notbid w = W ¬ q ˙ w ¬ q ˙ W
17 14 16 anbi12d w = W ¬ p ˙ w ¬ q ˙ w ¬ p ˙ W ¬ q ˙ W
18 oveq2 w = W p ˙ f p ˙ w = p ˙ f p ˙ W
19 oveq2 w = W q ˙ f q ˙ w = q ˙ f q ˙ W
20 18 19 eqeq12d w = W p ˙ f p ˙ w = q ˙ f q ˙ w p ˙ f p ˙ W = q ˙ f q ˙ W
21 17 20 imbi12d w = W ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W
22 21 2ralbidv w = W p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W
23 12 22 rabeqbidv w = W f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w = f D | p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W
24 eqid w H f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w = w H f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w
25 6 fvexi D V
26 25 rabex f D | p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W V
27 23 24 26 fvmpt W H w H f LDil K w | p A q A ¬ p ˙ w ¬ q ˙ w p ˙ f p ˙ w = q ˙ f q ˙ w W = f D | p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W
28 10 27 sylan9eq K B W H T = f D | p A q A ¬ p ˙ W ¬ q ˙ W p ˙ f p ˙ W = q ˙ f q ˙ W