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

Metamath Proof Explorer

Theorem ldilset

Description: The set of lattice dilations for a fiducial co-atom W . (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses ldilset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ldilset.l ⊢ ≤ = ( le ‘ 𝐾 )
ldilset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ldilset.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
ldilset.d ⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
Assertion ldilset ( ( 𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 ldilset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ldilset.l ⊢ ≤ = ( le ‘ 𝐾 )
3 ldilset.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 ldilset.i ⊢ 𝐼 = ( LAut ‘ 𝐾 )
5 ldilset.d ⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
6 1 2 3 4 ldilfset ⊢ ( 𝐾 ∈ 𝐶 → ( LDil ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
7 6 fveq1d ⊢ ( 𝐾 ∈ 𝐶 → ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ‘ 𝑊 ) )
8 breq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑥 ≤ 𝑤 ↔ 𝑥 ≤ 𝑊 ) )
9 8 imbi1d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) )
10 9 ralbidv ⊢ ( 𝑤 = 𝑊 → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) )
11 10 rabbidv ⊢ ( 𝑤 = 𝑊 → { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } = { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
12 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
13 4 fvexi ⊢ 𝐼 ∈ V
14 13 rabex ⊢ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ∈ V
15 11 12 14 fvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ‘ 𝑊 ) = { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
16 7 15 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻 ) → ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) = { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
17 5 16 eqtrid ⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )