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 𝐵 = ( Base ‘ 𝐾 )
ldilset.l = ( le ‘ 𝐾 )
ldilset.h 𝐻 = ( LHyp ‘ 𝐾 )
ldilset.i 𝐼 = ( LAut ‘ 𝐾 )
Assertion ldilfset ( 𝐾𝐶 → ( LDil ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑓𝐼 ∣ ∀ 𝑥𝐵 ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 ldilset.b 𝐵 = ( Base ‘ 𝐾 )
2 ldilset.l = ( le ‘ 𝐾 )
3 ldilset.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ldilset.i 𝐼 = ( LAut ‘ 𝐾 )
5 elex ( 𝐾𝐶𝐾 ∈ V )
6 fveq2 ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
7 6 3 eqtr4di ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
8 fveq2 ( 𝑘 = 𝐾 → ( LAut ‘ 𝑘 ) = ( LAut ‘ 𝐾 ) )
9 8 4 eqtr4di ( 𝑘 = 𝐾 → ( LAut ‘ 𝑘 ) = 𝐼 )
10 fveq2 ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) )
11 10 1 eqtr4di ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 )
12 fveq2 ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
13 12 2 eqtr4di ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = )
14 13 breqd ( 𝑘 = 𝐾 → ( 𝑥 ( le ‘ 𝑘 ) 𝑤𝑥 𝑤 ) )
15 14 imbi1d ( 𝑘 = 𝐾 → ( ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) ↔ ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) ) )
16 11 15 raleqbidv ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) ↔ ∀ 𝑥𝐵 ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) ) )
17 9 16 rabeqbidv ( 𝑘 = 𝐾 → { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } = { 𝑓𝐼 ∣ ∀ 𝑥𝐵 ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } )
18 7 17 mpteq12dv ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } ) = ( 𝑤𝐻 ↦ { 𝑓𝐼 ∣ ∀ 𝑥𝐵 ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } ) )
19 df-ldil LDil = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } ) )
20 18 19 3 mptfvmpt ( 𝐾 ∈ V → ( LDil ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑓𝐼 ∣ ∀ 𝑥𝐵 ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } ) )
21 5 20 syl ( 𝐾𝐶 → ( LDil ‘ 𝐾 ) = ( 𝑤𝐻 ↦ { 𝑓𝐼 ∣ ∀ 𝑥𝐵 ( 𝑥 𝑤 → ( 𝑓𝑥 ) = 𝑥 ) } ) )