ltrnnidn

Description: If a lattice translation is not the identity, then the translation of any atom not under the fiducial co-atom W is different from the atom. Remark above Lemma C in Crawley p. 112. (Contributed by NM, 24-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	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$

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		simp1l	$⊢ ((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 K \in HL$
7		hlatl	$⊢ K \in HL \to K \in AtLat$
8	6 7	syl	$⊢ ((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 K \in AtLat$
9		simp1	$⊢ ((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 (K \in HL \land W \in H)$
10		simp2l	$⊢ ((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 \in T$
11		simp2r	$⊢ ((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 \neq {I ↾}_{B}$
12		eqid	$⊢ trL (K) (W) = trL (K) (W)$
13	1 3 4 5 12	trlnidat	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to trL (K) (W) (F) \in A$
14	9 10 11 13	syl3anc	$⊢ ((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 trL (K) (W) (F) \in A$
15		eqid	$⊢ 0. (K) = 0. (K)$
16	15 3	atn0	$⊢ (K \in AtLat \land trL (K) (W) (F) \in A) \to trL (K) (W) (F) \neq 0. (K)$
17	8 14 16	syl2anc	$⊢ ((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 trL (K) (W) (F) \neq 0. (K)$
18		simpl1	$⊢ (((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)) \land F (P) = P) \to (K \in HL \land W \in H)$
19		simpl3	$⊢ (((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)) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
20		simpl2l	$⊢ (((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)) \land F (P) = P) \to F \in T$
21		simpr	$⊢ (((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)) \land F (P) = P) \to F (P) = P$
22	2 15 3 4 5 12	trl0	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) = P)) \to trL (K) (W) (F) = 0. (K)$
23	18 19 20 21 22	syl112anc	$⊢ (((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)) \land F (P) = P) \to trL (K) (W) (F) = 0. (K)$
24	23	ex	$⊢ ((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) = P \to trL (K) (W) (F) = 0. (K))$
25	24	necon3d	$⊢ ((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 (trL (K) (W) (F) \neq 0. (K) \to F (P) \neq P)$
26	17 25	mpd	$⊢ ((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$

Metamath Proof Explorer

Theorem ltrnnidn

Proof