ltrnideq

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

	Ref	Expression
Hypotheses	ltrnnidn.b	$⊢ B = {Base}_{K}$
	ltrnnidn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrnnidn.a	$⊢ A = Atoms (K)$
	ltrnnidn.h	$⊢ H = LHyp (K)$
	ltrnnidn.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnideq	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F = {I ↾}_{B} \leftrightarrow F (P) = P)$

Proof

Step	Hyp	Ref	Expression
1		ltrnnidn.b	$⊢ B = {Base}_{K}$
2		ltrnnidn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ltrnnidn.a	$⊢ A = Atoms (K)$
4		ltrnnidn.h	$⊢ H = LHyp (K)$
5		ltrnnidn.t	$⊢ T = LTrn (K) (W)$
6		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F = {I ↾}_{B}) \to F = {I ↾}_{B}$
7	6	fveq1d	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F = {I ↾}_{B}) \to F (P) = ({I ↾}_{B}) (P)$
8		simpl3l	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F = {I ↾}_{B}) \to P \in A$
9	1 3	atbase	$⊢ P \in A \to P \in B$
10		fvresi	$⊢ P \in B \to ({I ↾}_{B}) (P) = P$
11	8 9 10	3syl	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F = {I ↾}_{B}) \to ({I ↾}_{B}) (P) = P$
12	7 11	eqtrd	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F = {I ↾}_{B}) \to F (P) = P$
13	12	ex	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F = {I ↾}_{B} \to F (P) = P)$
14		simpl1	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F \neq {I ↾}_{B}) \to (K \in HL \land W \in H)$
15		simpl2	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F \neq {I ↾}_{B}) \to F \in T$
16		simpr	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F \neq {I ↾}_{B}) \to F \neq {I ↾}_{B}$
17		simpl3	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F \neq {I ↾}_{B}) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
18	1 2 3 4 5	ltrnnidn	$⊢ ((K \in HL \land W \in H) \land (F \in T \land F \neq {I ↾}_{B}) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \neq P$
19	14 15 16 17 18	syl121anc	$⊢ (((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F \neq {I ↾}_{B}) \to F (P) \neq P$
20	19	ex	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F \neq {I ↾}_{B} \to F (P) \neq P)$
21	20	necon4d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) = P \to F = {I ↾}_{B})$
22	13 21	impbid	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F = {I ↾}_{B} \leftrightarrow F (P) = P)$

Metamath Proof Explorer

Theorem ltrnideq

Proof