This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idldil

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

Ref Expression
Hypotheses idldil.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
idldil.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
idldil.d ⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
Assertion idldil ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 idldil.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 idldil.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 idldil.d ⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
4 eqid ⊢ ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
5 1 4 idlaut ⊢ ( 𝐾 ∈ 𝐴 → ( I ↾ 𝐵 ) ∈ ( LAut ‘ 𝐾 ) )
6 5 adantr ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ ( LAut ‘ 𝐾 ) )
7 fvresi ⊢ ( 𝑥 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
8 7 a1d ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 ) )
9 8 rgen ⊢ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
10 9 a1i ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 ) )
11 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12 1 11 2 4 3 isldil ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ( ( I ↾ 𝐵 ) ∈ 𝐷 ↔ ( ( I ↾ 𝐵 ) ∈ ( LAut ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑊 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 ) ) ) )
13 6 10 12 mpbir2and ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝐷 )