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 ↾ 𝐵 ) ∈ 𝐷 )