ltrnel

Description: The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in Crawley p. 112. (Contributed by NM, 22-May-2012)

	Ref	Expression
Hypotheses	ltrnel.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ltrnel.a	$⊢ A = Atoms (K)$
	ltrnel.h	$⊢ H = LHyp (K)$
	ltrnel.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$

Proof

Step	Hyp	Ref	Expression
1		ltrnel.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		ltrnel.a	$⊢ A = Atoms (K)$
3		ltrnel.h	$⊢ H = LHyp (K)$
4		ltrnel.t	$⊢ T = LTrn (K) (W)$
5		simp3l	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in A$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
8	7	adantr	$⊢ (P \in A \land \neg P \underset{˙}{\leq} W) \to P \in {Base}_{K}$
9	6 2 3 4	ltrnatb	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in {Base}_{K}) \to (P \in A \leftrightarrow F (P) \in A)$
10	8 9	syl3an3	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \in A \leftrightarrow F (P) \in A)$
11	5 10	mpbid	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (P) \in A$
12		simp3r	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg P \underset{˙}{\leq} W$
13		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (K \in HL \land W \in H)$
14		simp2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F \in T$
15	5 7	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \in {Base}_{K}$
16		simp1r	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in H$
17	6 3	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
19	6 1 3 4	ltrnle	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in {Base}_{K} \land W \in {Base}_{K})) \to (P \underset{˙}{\leq} W \leftrightarrow F (P) \underset{˙}{\leq} F (W))$
20	13 14 15 18 19	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \underset{˙}{\leq} W \leftrightarrow F (P) \underset{˙}{\leq} F (W))$
21		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in HL$
22	21	hllatd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in Lat$
23	6 1	latref	$⊢ (K \in Lat \land W \in {Base}_{K}) \to W \underset{˙}{\leq} W$
24	22 18 23	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \underset{˙}{\leq} W$
25	6 1 3 4	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (W \in {Base}_{K} \land W \underset{˙}{\leq} W)) \to F (W) = W$
26	13 14 18 24 25	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to F (W) = W$
27	26	breq2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \underset{˙}{\leq} F (W) \leftrightarrow F (P) \underset{˙}{\leq} W)$
28	20 27	bitrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \underset{˙}{\leq} W \leftrightarrow F (P) \underset{˙}{\leq} W)$
29	12 28	mtbid	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg F (P) \underset{˙}{\leq} W$
30	11 29	jca	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$

Metamath Proof Explorer

Theorem ltrnel

Proof