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=BaseK
ldilset.l ˙=K
ldilset.h H=LHypK
ldilset.i I=LAutK
Assertion ldilfset KCLDilK=wHfI|xBx˙wfx=x

Proof

Step Hyp Ref Expression
1 ldilset.b B=BaseK
2 ldilset.l ˙=K
3 ldilset.h H=LHypK
4 ldilset.i I=LAutK
5 elex KCKV
6 fveq2 k=KLHypk=LHypK
7 6 3 eqtr4di k=KLHypk=H
8 fveq2 k=KLAutk=LAutK
9 8 4 eqtr4di k=KLAutk=I
10 fveq2 k=KBasek=BaseK
11 10 1 eqtr4di k=KBasek=B
12 fveq2 k=Kk=K
13 12 2 eqtr4di k=Kk=˙
14 13 breqd k=Kxkwx˙w
15 14 imbi1d k=Kxkwfx=xx˙wfx=x
16 11 15 raleqbidv k=KxBasekxkwfx=xxBx˙wfx=x
17 9 16 rabeqbidv k=KfLAutk|xBasekxkwfx=x=fI|xBx˙wfx=x
18 7 17 mpteq12dv k=KwLHypkfLAutk|xBasekxkwfx=x=wHfI|xBx˙wfx=x
19 df-ldil LDil=kVwLHypkfLAutk|xBasekxkwfx=x
20 18 19 3 mptfvmpt KVLDilK=wHfI|xBx˙wfx=x
21 5 20 syl KCLDilK=wHfI|xBx˙wfx=x