trljat2

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. (Contributed by NM, 25-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	trljat2	$⊢ ((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{˙}{\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		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$
8	1 3 4 5	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
9	8	3adant3r	$⊢ ((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$
10	7	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$
11		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$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
14	11 13	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}$
15		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)$
16		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$
17	12 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}$
18	15 16 14 17	syl3anc	$⊢ ((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}$
19	12 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}$
20	10 14 18 19	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}$
21		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$
22	12 4	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
23	21 22	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}$
24	12 1 2	latlej2	$⊢ (K \in Lat \land P \in {Base}_{K} \land F (P) \in {Base}_{K}) \to F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
25	10 14 18 24	syl3anc	$⊢ ((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} (P \underset{˙}{\lor} F (P))$
26		eqid	$⊢ meet (K) = meet (K)$
27	12 1 2 26 3	atmod2i1	$⊢ (K \in HL \land (F (P) \in A \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land W \in {Base}_{K}) \land F (P) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to ((P \underset{˙}{\lor} F (P)) meet (K) W) \underset{˙}{\lor} F (P) = (P \underset{˙}{\lor} F (P)) meet (K) (W \underset{˙}{\lor} F (P))$
28	7 9 20 23 25 27	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} F (P) = (P \underset{˙}{\lor} F (P)) meet (K) (W \underset{˙}{\lor} F (P))$
29	1 3 4 5	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)$
30		eqid	$⊢ 1. (K) = 1. (K)$
31	1 2 30 3 4	lhpjat1	$⊢ ((K \in HL \land W \in H) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} F (P) = 1. (K)$
32	7 21 29 31	syl21anc	$⊢ ((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} F (P) = 1. (K)$
33	32	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} F (P)) = (P \underset{˙}{\lor} F (P)) meet (K) 1. (K)$
34		hlol	$⊢ K \in HL \to K \in OL$
35	7 34	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$
36	12 26 30	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)$
37	35 20 36	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)$
38	28 33 37	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} F (P)$
39	1 2 26 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$
40	39	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} F (P) = ((P \underset{˙}{\lor} F (P)) meet (K) W) \underset{˙}{\lor} F (P)$
41	12 4 5 6	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
42	15 16 41	syl2anc	$⊢ ((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}$
43	12 2	latjcom	$⊢ (K \in Lat \land R (F) \in {Base}_{K} \land F (P) \in {Base}_{K}) \to R (F) \underset{˙}{\lor} F (P) = F (P) \underset{˙}{\lor} R (F)$
44	10 42 18 43	syl3anc	$⊢ ((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} F (P) = F (P) \underset{˙}{\lor} R (F)$
45	38 40 44	3eqtr2rd	$⊢ ((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{˙}{\lor} R (F) = P \underset{˙}{\lor} F (P)$

Metamath Proof Explorer

Theorem trljat2

Proof