Metamath Proof Explorer


Theorem ldilfset

Description: The mapping from fiducial co-atom w to its set of lattice dilations. (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses ldilset.b B = Base K
ldilset.l ˙ = K
ldilset.h H = LHyp K
ldilset.i I = LAut K
Assertion ldilfset K C LDil K = w H f I | x B x ˙ w f x = x

Proof

Step Hyp Ref Expression
1 ldilset.b B = Base K
2 ldilset.l ˙ = K
3 ldilset.h H = LHyp K
4 ldilset.i I = LAut K
5 elex K C K V
6 fveq2 k = K LHyp k = LHyp K
7 6 3 eqtr4di k = K LHyp k = H
8 fveq2 k = K LAut k = LAut K
9 8 4 eqtr4di k = K LAut k = I
10 fveq2 k = K Base k = Base K
11 10 1 eqtr4di k = K Base k = B
12 fveq2 k = K k = K
13 12 2 eqtr4di k = K k = ˙
14 13 breqd k = K x k w x ˙ w
15 14 imbi1d k = K x k w f x = x x ˙ w f x = x
16 11 15 raleqbidv k = K x Base k x k w f x = x x B x ˙ w f x = x
17 9 16 rabeqbidv k = K f LAut k | x Base k x k w f x = x = f I | x B x ˙ w f x = x
18 7 17 mpteq12dv k = K w LHyp k f LAut k | x Base k x k w f x = x = w H f I | x B x ˙ w f x = x
19 df-ldil LDil = k V w LHyp k f LAut k | x Base k x k w f x = x
20 18 19 3 mptfvmpt K V LDil K = w H f I | x B x ˙ w f x = x
21 5 20 syl K C LDil K = w H f I | x B x ˙ w f x = x