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 ↾ 𝐵 ) ) )