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 ⊢A=Atoms⁡K
dilset.s ⊢S=PSubSp⁡K
dilset.w ⊢W=WAtoms⁡K
dilset.m ⊢M=PAut⁡K
dilset.l ⊢L=Dil⁡K
Assertion dilfsetN ⊢K∈B→L=d∈A⟼f∈M|∀x∈Sx⊆W⁡d→f⁡x=x

Proof

Step Hyp Ref Expression
1 dilset.a ⊢A=Atoms⁡K
2 dilset.s ⊢S=PSubSp⁡K
3 dilset.w ⊢W=WAtoms⁡K
4 dilset.m ⊢M=PAut⁡K
5 dilset.l ⊢L=Dil⁡K
6 elex ⊢K∈B→K∈V
7 fveq2 ⊢k=K→Atoms⁡k=Atoms⁡K
8 7 1 eqtr4di ⊢k=K→Atoms⁡k=A
9 fveq2 ⊢k=K→PAut⁡k=PAut⁡K
10 9 4 eqtr4di ⊢k=K→PAut⁡k=M
11 fveq2 ⊢k=K→PSubSp⁡k=PSubSp⁡K
12 11 2 eqtr4di ⊢k=K→PSubSp⁡k=S
13 fveq2 ⊢k=K→WAtoms⁡k=WAtoms⁡K
14 13 3 eqtr4di ⊢k=K→WAtoms⁡k=W
15 14 fveq1d ⊢k=K→WAtoms⁡k⁡d=W⁡d
16 15 sseq2d ⊢k=K→x⊆WAtoms⁡k⁡d↔x⊆W⁡d
17 16 imbi1d ⊢k=K→x⊆WAtoms⁡k⁡d→f⁡x=x↔x⊆W⁡d→f⁡x=x
18 12 17 raleqbidv ⊢k=K→∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x↔∀x∈Sx⊆W⁡d→f⁡x=x
19 10 18 rabeqbidv ⊢k=K→f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x=f∈M|∀x∈Sx⊆W⁡d→f⁡x=x
20 8 19 mpteq12dv ⊢k=K→d∈Atoms⁡k⟼f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x=d∈A⟼f∈M|∀x∈Sx⊆W⁡d→f⁡x=x
21 df-dilN ⊢Dil=k∈V⟼d∈Atoms⁡k⟼f∈PAut⁡k|∀x∈PSubSp⁡kx⊆WAtoms⁡k⁡d→f⁡x=x
22 20 21 1 mptfvmpt ⊢K∈V→Dil⁡K=d∈A⟼f∈M|∀x∈Sx⊆W⁡d→f⁡x=x
23 5 22 eqtrid ⊢K∈V→L=d∈A⟼f∈M|∀x∈Sx⊆W⁡d→f⁡x=x
24 6 23 syl ⊢K∈B→L=d∈A⟼f∈M|∀x∈Sx⊆W⁡d→f⁡x=x