Metamath Proof Explorer

Theorem dilfsetN

Description: The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses dilset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dilset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
dilset.w ⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
dilset.m ⊢ 𝑀 = ( PAut ‘ 𝐾 )
dilset.l ⊢ 𝐿 = ( Dil ‘ 𝐾 )
Assertion dilfsetN ( 𝐾 ∈ 𝐵 → 𝐿 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 dilset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 dilset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3 dilset.w ⊢ 𝑊 = ( WAtoms ‘ 𝐾 )
4 dilset.m ⊢ 𝑀 = ( PAut ‘ 𝐾 )
5 dilset.l ⊢ 𝐿 = ( Dil ‘ 𝐾 )
6 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
7 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
8 7 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
9 fveq2 ⊢ ( 𝑘 = 𝐾 → ( PAut ‘ 𝑘 ) = ( PAut ‘ 𝐾 ) )
10 9 4 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( PAut ‘ 𝑘 ) = 𝑀 )
11 fveq2 ⊢ ( 𝑘 = 𝐾 → ( PSubSp ‘ 𝑘 ) = ( PSubSp ‘ 𝐾 ) )
12 11 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( PSubSp ‘ 𝑘 ) = 𝑆 )
13 fveq2 ⊢ ( 𝑘 = 𝐾 → ( WAtoms ‘ 𝑘 ) = ( WAtoms ‘ 𝐾 ) )
14 13 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( WAtoms ‘ 𝑘 ) = 𝑊 )
15 14 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) = ( 𝑊 ‘ 𝑑 ) )
16 15 sseq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) ↔ 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) ) )
17 16 imbi1d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) )
18 12 17 raleqbidv ⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) )
19 10 18 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } = { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
20 8 19 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
21 df-dilN ⊢ Dil = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
22 20 21 1 mptfvmpt ⊢ ( 𝐾 ∈ V → ( Dil ‘ 𝐾 ) = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
23 5 22 syl5eq ⊢ ( 𝐾 ∈ V → 𝐿 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
24 6 23 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝐿 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )