Metamath Proof Explorer


Theorem ltrncvr

Description: Covering property of a lattice translation. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrncvr.b 𝐵 = ( Base ‘ 𝐾 )
ltrncvr.c 𝐶 = ( ⋖ ‘ 𝐾 )
ltrncvr.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrncvr.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrncvr ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 ltrncvr.b 𝐵 = ( Base ‘ 𝐾 )
2 ltrncvr.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 ltrncvr.h 𝐻 = ( LHyp ‘ 𝐾 )
4 ltrncvr.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 simp1l ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝐾𝑉 )
6 eqid ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
7 3 6 4 ltrnlaut ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
8 7 3adant3 ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
9 simp3l ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑋𝐵 )
10 simp3r ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → 𝑌𝐵 )
11 1 2 6 lautcvr ( ( 𝐾𝑉 ∧ ( 𝐹 ∈ ( LAut ‘ 𝐾 ) ∧ 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ) )
12 5 8 9 10 11 syl13anc ( ( ( 𝐾𝑉𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑋𝐵𝑌𝐵 ) ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝐹𝑋 ) 𝐶 ( 𝐹𝑌 ) ) )