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

Metamath Proof Explorer

Theorem ltrnval1

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

Ref Expression
Hypotheses ltrnval1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ltrnval1.l ⊢ ≤ = ( le ‘ 𝐾 )
ltrnval1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrnval1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnval1 ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 ltrnval1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ltrnval1.l ⊢ ≤ = ( le ‘ 𝐾 )
3 ltrnval1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrnval1.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ⊢ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LDil ‘ 𝐾 ) ‘ 𝑊 )
6 3 5 4 ltrnldil ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) )
7 6 3adant3 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) )
8 1 2 3 5 ldilval ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ ( ( LDil ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )
9 7 8 syld3an2 ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )