trljat1

Description: The value of a translation of an atom P not under the fiducial co-atom W , joined with trace. Equation above Lemma C in Crawley p. 112. TODO: shorten with atmod3i1 ? (Contributed by NM, 22-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		trljat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trljat.j	$⊢ \underset{˙}{\lor} = join (K)$
3		trljat.a	$⊢ A = Atoms (K)$
4		trljat.h	$⊢ H = LHyp (K)$
5		trljat.t	$⊢ T = LTrn (K) (W)$
6		trljat.r	$⊢ R = trL (K) (W)$
7		eqid	$⊢ meet (K) = meet (K)$
8	1 2 7 3 4 5 6	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) = (P \underset{˙}{\lor} F (P)) meet (K) W$
9	8	oveq1d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) \underset{˙}{\lor} P = ((P \underset{˙}{\lor} F (P)) meet (K) W) \underset{˙}{\lor} P$
10		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$
11	10	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$
12		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$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
15	12 14	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	13 4 5 6	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
17	16	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to R (F) \in {Base}_{K}$
18	13 2	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land R (F) \in {Base}_{K}) \to P \underset{˙}{\lor} R (F) = R (F) \underset{˙}{\lor} P$
19	11 15 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (F) = R (F) \underset{˙}{\lor} P$
20	13 4 5	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in {Base}_{K}) \to F (P) \in {Base}_{K}$
21	15 20	syld3an3	$⊢ ((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 {Base}_{K}$
22	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land F (P) \in {Base}_{K}) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
23	11 15 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
24		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$
25	13 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
26	24 25	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}$
27	13 1 2	latlej1	$⊢ (K \in Lat \land P \in {Base}_{K} \land F (P) \in {Base}_{K}) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
28	11 15 21 27	syl3anc	$⊢ ((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} (P \underset{˙}{\lor} F (P))$
29	13 1 2 7 3	atmod2i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land W \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to ((P \underset{˙}{\lor} F (P)) meet (K) W) \underset{˙}{\lor} P = (P \underset{˙}{\lor} F (P)) meet (K) (W \underset{˙}{\lor} P)$
30	10 12 23 26 28 29	syl131anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to ((P \underset{˙}{\lor} F (P)) meet (K) W) \underset{˙}{\lor} P = (P \underset{˙}{\lor} F (P)) meet (K) (W \underset{˙}{\lor} P)$
31		eqid	$⊢ 1. (K) = 1. (K)$
32	1 2 31 3 4	lhpjat1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} P = 1. (K)$
33	32	3adant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} P = 1. (K)$
34	33	oveq2d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} F (P)) meet (K) (W \underset{˙}{\lor} P) = (P \underset{˙}{\lor} F (P)) meet (K) 1. (K)$
35		hlol	$⊢ K \in HL \to K \in OL$
36	10 35	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to K \in OL$
37	13 7 31	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} F (P) \in {Base}_{K}) \to (P \underset{˙}{\lor} F (P)) meet (K) 1. (K) = P \underset{˙}{\lor} F (P)$
38	36 23 37	syl2anc	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (P \underset{˙}{\lor} F (P)) meet (K) 1. (K) = P \underset{˙}{\lor} F (P)$
39	30 34 38	3eqtrrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} F (P) = ((P \underset{˙}{\lor} F (P)) meet (K) W) \underset{˙}{\lor} P$
40	9 19 39	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} R (F) = P \underset{˙}{\lor} F (P)$

Metamath Proof Explorer

Theorem trljat1

Proof