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 ↾ 𝐵 ) ↔ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) )