Metamath Proof Explorer


Theorem ltrnm

Description: Lattice translation of a meet. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrnm.b 𝐵 = ( Base ‘ 𝐾 )
ltrnm.m = ( meet ‘ 𝐾 )
ltrnm.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnm.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnm ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 ltrnm.b 𝐵 = ( Base ‘ 𝐾 )
2 ltrnm.m = ( meet ‘ 𝐾 )
3 ltrnm.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrnm.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝐾 ∈ HL )
6 5 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝐾 ∈ Lat )
7 eqid ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
8 3 7 4 ltrnlaut ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
9 8 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
10 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
11 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
12 1 2 7 lautm ( ( 𝐾 ∈ Lat ∧ ( 𝐹 ∈ ( LAut ‘ 𝐾 ) ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )
13 6 9 10 11 12 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝐹 ‘ ( 𝑋 𝑌 ) ) = ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )