This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltrnid

Description: A lattice translation is the identity function iff all atoms not under the fiducial co-atom W are equal to their values. (Contributed by NM, 24-May-2012)

Ref Expression
Hypotheses ltrneq.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ltrneq.l ⊢ ≤ = ( le ‘ 𝐾 )
ltrneq.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
ltrneq.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
ltrneq.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrnid ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ↔ 𝐹 = ( I ↾ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ltrneq.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ltrneq.l ⊢ ≤ = ( le ‘ 𝐾 )
3 ltrneq.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 ltrneq.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 ltrneq.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
6 simp-4l ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐾 ∈ HL )
7 eqid ⊢ ( LAut ‘ 𝐾 ) = ( LAut ‘ 𝐾 )
8 4 7 5 ltrnlaut ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
9 8 ad2antrr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐹 ∈ ( LAut ‘ 𝐾 ) )
10 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
11 simplll ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ≤ 𝑊 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ≤ 𝑊 ) → 𝐹 ∈ 𝑇 )
13 1 3 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
14 13 ad2antlr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ≤ 𝑊 ) → 𝑝 ∈ 𝐵 )
15 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ≤ 𝑊 ) → 𝑝 ≤ 𝑊 )
16 1 2 4 5 ltrnval1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑝 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 )
17 11 12 14 15 16 syl112anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) ∧ 𝑝 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 )
18 17 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
19 pm2.61 ⊢ ( ( 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
20 18 19 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
21 20 ralimdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
22 21 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 )
23 22 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 )
24 1 3 7 lauteq ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝐹 ∈ ( LAut ‘ 𝐾 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
25 6 9 10 23 24 syl31anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 )
26 fvresi ⊢ ( 𝑥 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
27 26 adantl ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
28 25 27 eqtr4d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐵 ) ‘ 𝑥 ) )
29 28 ralrimiva ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐵 ) ‘ 𝑥 ) )
30 1 4 5 ltrn1o ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
31 30 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → 𝐹 : 𝐵 –1-1-onto→ 𝐵 )
32 f1ofn ⊢ ( 𝐹 : 𝐵 –1-1-onto→ 𝐵 → 𝐹 Fn 𝐵 )
33 31 32 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → 𝐹 Fn 𝐵 )
34 fnresi ⊢ ( I ↾ 𝐵 ) Fn 𝐵
35 eqfnfv ⊢ ( ( 𝐹 Fn 𝐵 ∧ ( I ↾ 𝐵 ) Fn 𝐵 ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) )
36 33 34 35 sylancl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ) )
37 29 36 mpbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) → 𝐹 = ( I ↾ 𝐵 ) )
38 37 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) → 𝐹 = ( I ↾ 𝐵 ) ) )
39 13 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
40 fvresi ⊢ ( 𝑝 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 )
41 39 40 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 )
42 fveq1 ⊢ ( 𝐹 = ( I ↾ 𝐵 ) → ( 𝐹 ‘ 𝑝 ) = ( ( I ↾ 𝐵 ) ‘ 𝑝 ) )
43 42 eqeq1d ⊢ ( 𝐹 = ( I ↾ 𝐵 ) → ( ( 𝐹 ‘ 𝑝 ) = 𝑝 ↔ ( ( I ↾ 𝐵 ) ‘ 𝑝 ) = 𝑝 ) )
44 41 43 syl5ibrcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝐹 = ( I ↾ 𝐵 ) → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) )
45 44 a1dd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝐹 = ( I ↾ 𝐵 ) → ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) )
46 45 ralrimdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐹 = ( I ↾ 𝐵 ) → ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ) )
47 38 46 impbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∀ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 → ( 𝐹 ‘ 𝑝 ) = 𝑝 ) ↔ 𝐹 = ( I ↾ 𝐵 ) ) )