Metamath Proof Explorer


Theorem ltrnideq

Description: Property of the identity lattice translation. (Contributed by NM, 27-May-2012)

Ref Expression
Hypotheses ltrnnidn.b 𝐵 = ( Base ‘ 𝐾 )
ltrnnidn.l = ( le ‘ 𝐾 )
ltrnnidn.a 𝐴 = ( Atoms ‘ 𝐾 )
ltrnnidn.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrnnidn.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnideq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝐹𝑃 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ltrnnidn.b 𝐵 = ( Base ‘ 𝐾 )
2 ltrnnidn.l = ( le ‘ 𝐾 )
3 ltrnnidn.a 𝐴 = ( Atoms ‘ 𝐾 )
4 ltrnnidn.h 𝐻 = ( LHyp ‘ 𝐾 )
5 ltrnnidn.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → 𝐹 = ( I ↾ 𝐵 ) )
7 6 fveq1d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝐹𝑃 ) = ( ( I ↾ 𝐵 ) ‘ 𝑃 ) )
8 simpl3l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → 𝑃𝐴 )
9 1 3 atbase ( 𝑃𝐴𝑃𝐵 )
10 fvresi ( 𝑃𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑃 ) = 𝑃 )
11 8 9 10 3syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑃 ) = 𝑃 )
12 7 11 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → ( 𝐹𝑃 ) = 𝑃 )
13 12 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) → ( 𝐹𝑃 ) = 𝑃 ) )
14 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
15 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹𝑇 )
16 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
17 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
18 1 2 3 4 5 ltrnnidn ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹𝑃 ) ≠ 𝑃 )
19 14 15 16 17 18 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) ∧ 𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝐹𝑃 ) ≠ 𝑃 )
20 19 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) → ( 𝐹𝑃 ) ≠ 𝑃 ) )
21 20 necon4d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝐹𝑃 ) = 𝑃𝐹 = ( I ↾ 𝐵 ) ) )
22 13 21 impbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ( 𝐹𝑃 ) = 𝑃 ) )