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