This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )