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

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝐷 → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑊 → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) ) )
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 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝐷 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )