Metamath Proof Explorer

Theorem idldil

Description: The identity function is a lattice dilation. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses idldil.b ⊢ B = Base K
idldil.h ⊢ H = LHyp ⁡ K
idldil.d ⊢ D = LDil ⁡ K ⁡ W
Assertion idldil ⊢ K ∈ A ∧ W ∈ H → I ↾ B ∈ D

Proof

Step Hyp Ref Expression
1 idldil.b ⊢ B = Base K
2 idldil.h ⊢ H = LHyp ⁡ K
3 idldil.d ⊢ D = LDil ⁡ K ⁡ W
4 eqid ⊢ LAut ⁡ K = LAut ⁡ K
5 1 4 idlaut ⊢ K ∈ A → I ↾ B ∈ LAut ⁡ K
6 5 adantr ⊢ K ∈ A ∧ W ∈ H → I ↾ B ∈ LAut ⁡ K
7 fvresi ⊢ x ∈ B → I ↾ B ⁡ x = x
8 7 a1d ⊢ x ∈ B → x ≤ K W → I ↾ B ⁡ x = x
9 8 rgen ⊢ ∀ x ∈ B x ≤ K W → I ↾ B ⁡ x = x
10 9 a1i ⊢ K ∈ A ∧ W ∈ H → ∀ x ∈ B x ≤ K W → I ↾ B ⁡ x = x
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 4 3 isldil ⊢ K ∈ A ∧ W ∈ H → I ↾ B ∈ D ↔ I ↾ B ∈ LAut ⁡ K ∧ ∀ x ∈ B x ≤ K W → I ↾ B ⁡ x = x
13 6 10 12 mpbir2and ⊢ K ∈ A ∧ W ∈ H → I ↾ B ∈ D