Theorem ldilval

Description: Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ldilval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ldilval.l	⊢ ≤ = ( le ‘ 𝐾 )
	ldilval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	ldilval.d	⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
Assertion	ldilval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝐷 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		ldilval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ldilval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		ldilval.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		ldilval.d	⊢ 𝐷 = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
5		eqid	⊢ ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
6	1 2 3 5 4	isldil	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 ∈ ( LAut ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) ) )
7		simpr	⊢ ( ( 𝐹 ∈ ( LAut ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) )
8	6 7	syl6bi	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝐷 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
9		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑊 ↔ 𝑋 ≤ 𝑊 ) )
10		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
11		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
12	10 11	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
13	9 12	imbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑋 ≤ 𝑊 → ( 𝐹 ‘ 𝑋 ) = 𝑋 ) ) )
14	13	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( 𝑋 ∈ 𝐵 → ( 𝑋 ≤ 𝑊 → ( 𝐹 ‘ 𝑋 ) = 𝑋 ) ) )
15	14	impd	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) → ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 ) )
16	8 15	syl6	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝐷 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 ) ) )
17	16	3imp	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝐷 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )