ltrnatb

Description: The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012)

	Ref	Expression
Hypotheses	ltrnatb.b	$⊢ B = {Base}_{K}$
	ltrnatb.a	$⊢ A = Atoms (K)$
	ltrnatb.h	$⊢ H = LHyp (K)$
	ltrnatb.t	$⊢ T = LTrn (K) (W)$
Assertion	ltrnatb	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (P \in A \leftrightarrow F (P) \in A)$

Proof

Step	Hyp	Ref	Expression
1		ltrnatb.b	$⊢ B = {Base}_{K}$
2		ltrnatb.a	$⊢ A = Atoms (K)$
3		ltrnatb.h	$⊢ H = LHyp (K)$
4		ltrnatb.t	$⊢ T = LTrn (K) (W)$
5		simp3	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to P \in B$
6	1 3 4	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to F (P) \in B$
7	5 6	2thd	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (P \in B \leftrightarrow F (P) \in B)$
8		simp1	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (K \in HL \land W \in H)$
9		simp2	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to F \in T$
10		simp1l	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to K \in HL$
11		hlop	$⊢ K \in HL \to K \in OP$
12		eqid	$⊢ 0. (K) = 0. (K)$
13	1 12	op0cl	$⊢ K \in OP \to 0. (K) \in B$
14	10 11 13	3syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to 0. (K) \in B$
15		eqid	$⊢ ⋖_{K} = ⋖_{K}$
16	1 15 3 4	ltrncvr	$⊢ ((K \in HL \land W \in H) \land F \in T \land (0. (K) \in B \land P \in B)) \to (0. (K) ⋖_{K} P \leftrightarrow F (0. (K)) ⋖_{K} F (P))$
17	8 9 14 5 16	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (0. (K) ⋖_{K} P \leftrightarrow F (0. (K)) ⋖_{K} F (P))$
18	10 11	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to K \in OP$
19		simp1r	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to W \in H$
20	1 3	lhpbase	$⊢ W \in H \to W \in B$
21	19 20	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to W \in B$
22		eqid	$⊢ \leq_{K} = \leq_{K}$
23	1 22 12	op0le	$⊢ (K \in OP \land W \in B) \to 0. (K) \leq_{K} W$
24	18 21 23	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to 0. (K) \leq_{K} W$
25	1 22 3 4	ltrnval1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (0. (K) \in B \land 0. (K) \leq_{K} W)) \to F (0. (K)) = 0. (K)$
26	8 9 14 24 25	syl112anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to F (0. (K)) = 0. (K)$
27	26	breq1d	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (F (0. (K)) ⋖_{K} F (P) \leftrightarrow 0. (K) ⋖_{K} F (P))$
28	17 27	bitrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (0. (K) ⋖_{K} P \leftrightarrow 0. (K) ⋖_{K} F (P))$
29	7 28	anbi12d	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to ((P \in B \land 0. (K) ⋖_{K} P) \leftrightarrow (F (P) \in B \land 0. (K) ⋖_{K} F (P)))$
30	1 12 15 2	isat	$⊢ K \in HL \to (P \in A \leftrightarrow (P \in B \land 0. (K) ⋖_{K} P))$
31	10 30	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (P \in A \leftrightarrow (P \in B \land 0. (K) ⋖_{K} P))$
32	1 12 15 2	isat	$⊢ K \in HL \to (F (P) \in A \leftrightarrow (F (P) \in B \land 0. (K) ⋖_{K} F (P)))$
33	10 32	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (F (P) \in A \leftrightarrow (F (P) \in B \land 0. (K) ⋖_{K} F (P)))$
34	29 31 33	3bitr4d	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in B) \to (P \in A \leftrightarrow F (P) \in A)$

Metamath Proof Explorer

Theorem ltrnatb

Proof