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	$⊢ B = {Base}_{K}$
	ltrneq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrneq.a	$⊢ A = Atoms (K)$
	ltrneq.h	$⊢ H = LHyp (K)$
	ltrneq.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p) \leftrightarrow F = {I ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		ltrneq.b	$⊢ B = {Base}_{K}$
2		ltrneq.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ltrneq.a	$⊢ A = Atoms (K)$
4		ltrneq.h	$⊢ H = LHyp (K)$
5		ltrneq.t	$⊢ T = LTrn (K) (W)$
6		simp-4l	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to K \in HL$
7		eqid	$⊢ LAut (K) = LAut (K)$
8	4 7 5	ltrnlaut	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in LAut (K)$
9	8	ad2antrr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to F \in LAut (K)$
10		simpr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to x \in B$
11		simplll	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land p \in A) \land p \underset{˙}{\leq} W) \to (K \in HL \land W \in H)$
12		simpllr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land p \in A) \land p \underset{˙}{\leq} W) \to F \in T$
13	1 3	atbase	$⊢ p \in A \to p \in B$
14	13	ad2antlr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land p \in A) \land p \underset{˙}{\leq} W) \to p \in B$
15		simpr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land p \in A) \land p \underset{˙}{\leq} W) \to p \underset{˙}{\leq} W$
16	1 2 4 5	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (p \in B \land p \underset{˙}{\leq} W)) \to F (p) = p$
17	11 12 14 15 16	syl112anc	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land p \in A) \land p \underset{˙}{\leq} W) \to F (p) = p$
18	17	ex	$⊢ (((K \in HL \land W \in H) \land F \in T) \land p \in A) \to (p \underset{˙}{\leq} W \to F (p) = p)$
19		pm2.61	$⊢ (p \underset{˙}{\leq} W \to F (p) = p) \to ((\neg p \underset{˙}{\leq} W \to F (p) = p) \to F (p) = p)$
20	18 19	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land p \in A) \to ((\neg p \underset{˙}{\leq} W \to F (p) = p) \to F (p) = p)$
21	20	ralimdva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p) \to \forall p \in A F (p) = p)$
22	21	imp	$⊢ (((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \to \forall p \in A F (p) = p$
23	22	adantr	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to \forall p \in A F (p) = p$
24	1 3 7	lauteq	$⊢ ((K \in HL \land F \in LAut (K) \land x \in B) \land \forall p \in A F (p) = p) \to F (x) = x$
25	6 9 10 23 24	syl31anc	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to F (x) = x$
26		fvresi	$⊢ x \in B \to ({I ↾}_{B}) (x) = x$
27	26	adantl	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to ({I ↾}_{B}) (x) = x$
28	25 27	eqtr4d	$⊢ ((((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \land x \in B) \to F (x) = ({I ↾}_{B}) (x)$
29	28	ralrimiva	$⊢ (((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \to \forall x \in B F (x) = ({I ↾}_{B}) (x)$
30	1 4 5	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
31	30	adantr	$⊢ (((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \to F : B \underset{1-1 onto}{⟶} B$
32		f1ofn	$⊢ F : B \underset{1-1 onto}{⟶} B \to F Fn B$
33	31 32	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \to F Fn B$
34		fnresi	$⊢ ({I ↾}_{B}) Fn B$
35		eqfnfv	$⊢ (F Fn B \land ({I ↾}_{B}) Fn B) \to (F = {I ↾}_{B} \leftrightarrow \forall x \in B F (x) = ({I ↾}_{B}) (x))$
36	33 34 35	sylancl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \to (F = {I ↾}_{B} \leftrightarrow \forall x \in B F (x) = ({I ↾}_{B}) (x))$
37	29 36	mpbird	$⊢ (((K \in HL \land W \in H) \land F \in T) \land \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p)) \to F = {I ↾}_{B}$
38	37	ex	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p) \to F = {I ↾}_{B})$
39	13	adantl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land p \in A) \to p \in B$
40		fvresi	$⊢ p \in B \to ({I ↾}_{B}) (p) = p$
41	39 40	syl	$⊢ (((K \in HL \land W \in H) \land F \in T) \land p \in A) \to ({I ↾}_{B}) (p) = p$
42		fveq1	$⊢ F = {I ↾}_{B} \to F (p) = ({I ↾}_{B}) (p)$
43	42	eqeq1d	$⊢ F = {I ↾}_{B} \to (F (p) = p \leftrightarrow ({I ↾}_{B}) (p) = p)$
44	41 43	syl5ibrcom	$⊢ (((K \in HL \land W \in H) \land F \in T) \land p \in A) \to (F = {I ↾}_{B} \to F (p) = p)$
45	44	a1dd	$⊢ (((K \in HL \land W \in H) \land F \in T) \land p \in A) \to (F = {I ↾}_{B} \to (\neg p \underset{˙}{\leq} W \to F (p) = p))$
46	45	ralrimdva	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F = {I ↾}_{B} \to \forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p))$
47	38 46	impbid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (\forall p \in A (\neg p \underset{˙}{\leq} W \to F (p) = p) \leftrightarrow F = {I ↾}_{B})$

Metamath Proof Explorer

Theorem ltrnid

Proof