trlval4

Description: The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		trlval3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		trlval3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		trlval3.m	$⊢ \underset{˙}{\land} = meet (K)$
4		trlval3.a	$⊢ A = Atoms (K)$
5		trlval3.h	$⊢ H = LHyp (K)$
6		trlval3.t	$⊢ T = LTrn (K) (W)$
7		trlval3.r	$⊢ R = trL (K) (W)$
8		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
9		simp21	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in T$
10		simp22	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
11		simp23	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
12		simp3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
13		simpl1l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to K \in HL$
14		simp23l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
15	14	adantr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to Q \in A$
16		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to (K \in HL \land W \in H)$
17		simpl21	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to F \in T$
18	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in A) \to F (Q) \in A$
19	16 17 15 18	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to F (Q) \in A$
20	1 2 4	hlatlej1	$⊢ (K \in HL \land Q \in A \land F (Q) \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
21	13 15 19 20	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
22		simpl22	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
23	1 2 4 5 6 7	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)$
24	16 17 22 23	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to P \underset{˙}{\lor} R (F) = P \underset{˙}{\lor} F (P)$
25		simpr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)$
26	24 25	eqtrd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to P \underset{˙}{\lor} R (F) = Q \underset{˙}{\lor} F (Q)$
27	21 26	breqtrrd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F))$
28		simpl3r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
29		simpll1	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to (K \in HL \land W \in H)$
30	22	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
31	17	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to F \in T$
32		simpr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to F (P) = P$
33		eqid	$⊢ 0. (K) = 0. (K)$
34	1 33 4 5 6 7	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 R (F) = 0. (K)$
35	29 30 31 32 34	syl112anc	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to R (F) = 0. (K)$
36		hlatl	$⊢ K \in HL \to K \in AtLat$
37	13 36	syl	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to K \in AtLat$
38		simp22l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
39	38	adantr	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to P \in A$
40		eqid	$⊢ {Base}_{K} = {Base}_{K}$
41	40 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
42	13 39 15 41	syl3anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
43	40 1 33	atl0le	$⊢ (K \in AtLat \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to 0. (K) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
44	37 42 43	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to 0. (K) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
45	44	adantr	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to 0. (K) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
46	35 45	eqbrtrd	$⊢ ((((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \land F (P) = P) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
47	46	ex	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to (F (P) = P \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
48	47	necon3bd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to F (P) \neq P)$
49	28 48	mpd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to F (P) \neq P$
50	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
51	16 22 17 49 50	syl112anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to R (F) \in A$
52		simpl3l	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to P \neq Q$
53	52	necomd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to Q \neq P$
54	1 2 4	hlatexch1	$⊢ (K \in HL \land (Q \in A \land R (F) \in A \land P \in A) \land Q \neq P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
55	13 15 51 39 53 54	syl131anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R (F)) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
56	27 55	mpd	$⊢ (((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q)) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
57	56	ex	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} F (P) = Q \underset{˙}{\lor} F (Q) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
58	57	necon3bd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))$
59	12 58	mpd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q)$
60	1 2 3 4 5 6 7	trlval3	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))$
61	8 9 10 11 59 60	syl113anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))$

Metamath Proof Explorer

Theorem trlval4

Proof