Metamath Proof Explorer

Theorem isdilN

Description: The predicate "is a dilation". (Contributed by NM, 4-Feb-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 isdilN ⊢ K ∈ B ∧ D ∈ A → F ∈ L ⁡ D ↔ F ∈ M ∧ ∀ x ∈ S x ⊆ 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 1 2 3 4 5 dilsetN ⊢ K ∈ B ∧ D ∈ A → L ⁡ D = f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x
7 6 eleq2d ⊢ K ∈ B ∧ D ∈ A → F ∈ L ⁡ D ↔ F ∈ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x
8 fveq1 ⊢ f = F → f ⁡ x = F ⁡ x
9 8 eqeq1d ⊢ f = F → f ⁡ x = x ↔ F ⁡ x = x
10 9 imbi2d ⊢ f = F → x ⊆ W ⁡ D → f ⁡ x = x ↔ x ⊆ W ⁡ D → F ⁡ x = x
11 10 ralbidv ⊢ f = F → ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x ↔ ∀ x ∈ S x ⊆ W ⁡ D → F ⁡ x = x
12 11 elrab ⊢ F ∈ f ∈ M | ∀ x ∈ S x ⊆ W ⁡ D → f ⁡ x = x ↔ F ∈ M ∧ ∀ x ∈ S x ⊆ W ⁡ D → F ⁡ x = x
13 7 12 bitrdi ⊢ K ∈ B ∧ D ∈ A → F ∈ L ⁡ D ↔ F ∈ M ∧ ∀ x ∈ S x ⊆ W ⁡ D → F ⁡ x = x