Metamath Proof Explorer

Theorem isldil

Description: The predicate "is a lattice dilation". Similar to definition of dilation in Crawley p. 111. (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses ldilset.b ⊢ B = Base K
ldilset.l ⊢ ≤ ˙ = ≤ K
ldilset.h ⊢ H = LHyp ⁡ K
ldilset.i ⊢ I = LAut ⁡ K
ldilset.d ⊢ D = LDil ⁡ K ⁡ W
Assertion isldil ⊢ K ∈ C ∧ W ∈ H → F ∈ D ↔ F ∈ I ∧ ∀ x ∈ B x ≤ ˙ W → F ⁡ x = x

Proof

Step Hyp Ref Expression
1 ldilset.b ⊢ B = Base K
2 ldilset.l ⊢ ≤ ˙ = ≤ K
3 ldilset.h ⊢ H = LHyp ⁡ K
4 ldilset.i ⊢ I = LAut ⁡ K
5 ldilset.d ⊢ D = LDil ⁡ K ⁡ W
6 1 2 3 4 5 ldilset ⊢ K ∈ C ∧ W ∈ H → D = f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x
7 6 eleq2d ⊢ K ∈ C ∧ W ∈ H → F ∈ D ↔ F ∈ f ∈ I | ∀ x ∈ B x ≤ ˙ W → 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 → f ⁡ x = x ↔ x ≤ ˙ W → F ⁡ x = x
11 10 ralbidv ⊢ f = F → ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x ↔ ∀ x ∈ B x ≤ ˙ W → F ⁡ x = x
12 11 elrab ⊢ F ∈ f ∈ I | ∀ x ∈ B x ≤ ˙ W → f ⁡ x = x ↔ F ∈ I ∧ ∀ x ∈ B x ≤ ˙ W → F ⁡ x = x
13 7 12 bitrdi ⊢ K ∈ C ∧ W ∈ H → F ∈ D ↔ F ∈ I ∧ ∀ x ∈ B x ≤ ˙ W → F ⁡ x = x