Theorem dilsetN

Description: The set of dilations for a fiducial atom D . (Contributed by NM, 4-Feb-2012) (New usage is discouraged.)

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

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	1 2 3 4 5	dilfsetN	⊢ ( 𝐾 ∈ 𝐵 → 𝐿 = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
7	6	fveq1d	⊢ ( 𝐾 ∈ 𝐵 → ( 𝐿 ‘ 𝐷 ) = ( ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ‘ 𝐷 ) )
8		fveq2	⊢ ( 𝑑 = 𝐷 → ( 𝑊 ‘ 𝑑 ) = ( 𝑊 ‘ 𝐷 ) )
9	8	sseq2d	⊢ ( 𝑑 = 𝐷 → ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) ↔ 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) ) )
10	9	imbi1d	⊢ ( 𝑑 = 𝐷 → ( ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) )
11	10	ralbidv	⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) )
12	11	rabbidv	⊢ ( 𝑑 = 𝐷 → { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } = { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
13		eqid	⊢ ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) = ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
14	4	fvexi	⊢ 𝑀 ∈ V
15	14	rabex	⊢ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ∈ V
16	12 13 15	fvmpt	⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑑 ∈ 𝐴 ↦ { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ‘ 𝐷 ) = { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
17	7 16	sylan9eq	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴 ) → ( 𝐿 ‘ 𝐷 ) = { 𝑓 ∈ 𝑀 ∣ ∀ 𝑥 ∈ 𝑆 ( 𝑥 ⊆ ( 𝑊 ‘ 𝐷 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )