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 ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑋 𝑊 ) ) → ( 𝐹𝑋 ) = 𝑋 )