trlval3

Description: The value of the trace of a lattice translation in terms of 2 atoms. TODO: Try to shorten proof. (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	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))$

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		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to (K \in HL \land W \in H)$
9		simpl31	$⊢ (((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))) \land F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
10		simpl2	$⊢ (((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))) \land F (P) = P) \to F \in T$
11		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to F (P) = P$
12		eqid	$⊢ 0. (K) = 0. (K)$
13	1 12 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)$
14	8 9 10 11 13	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to R (F) = 0. (K)$
15		simpl33	$⊢ (((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))) \land F (P) = P) \to P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q)$
16		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to K \in HL$
17		hlatl	$⊢ K \in HL \to K \in AtLat$
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) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to K \in AtLat$
19	11	oveq2d	$⊢ (((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))) \land F (P) = P) \to P \underset{˙}{\lor} F (P) = P \underset{˙}{\lor} P$
20		simp31l	$⊢ ((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 P \in A$
21	20	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to P \in A$
22	2 4	hlatjidm	$⊢ (K \in HL \land P \in A) \to P \underset{˙}{\lor} P = P$
23	16 21 22	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to P \underset{˙}{\lor} P = P$
24	19 23	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to P \underset{˙}{\lor} F (P) = P$
25	24 21	eqeltrd	$⊢ (((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))) \land F (P) = P) \to P \underset{˙}{\lor} F (P) \in A$
26		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \to (K \in HL \land W \in H)$
27		simp2	$⊢ ((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 F \in T$
28		simp31	$⊢ ((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 (P \in A \land \neg P \underset{˙}{\leq} W)$
29		simp32	$⊢ ((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 (Q \in A \land \neg Q \underset{˙}{\leq} W)$
30	1 4 5 6	ltrn2ateq	$⊢ ((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))) \to (F (P) = P \leftrightarrow F (Q) = Q)$
31	26 27 28 29 30	syl13anc	$⊢ ((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 (F (P) = P \leftrightarrow F (Q) = Q)$
32	31	biimpa	$⊢ (((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))) \land F (P) = P) \to F (Q) = Q$
33	32	oveq2d	$⊢ (((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))) \land F (P) = P) \to Q \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} Q$
34		simp32l	$⊢ ((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 Q \in A$
35	34	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to Q \in A$
36	2 4	hlatjidm	$⊢ (K \in HL \land Q \in A) \to Q \underset{˙}{\lor} Q = Q$
37	16 35 36	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to Q \underset{˙}{\lor} Q = Q$
38	33 37	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to Q \underset{˙}{\lor} F (Q) = Q$
39	38 35	eqeltrd	$⊢ (((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))) \land F (P) = P) \to Q \underset{˙}{\lor} F (Q) \in A$
40	3 12 4	atnem0	$⊢ (K \in AtLat \land P \underset{˙}{\lor} F (P) \in A \land Q \underset{˙}{\lor} F (Q) \in A) \to (P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q) \leftrightarrow (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K))$
41	18 25 39 40	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) = P) \to (P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q) \leftrightarrow (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K))$
42	15 41	mpbid	$⊢ (((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))) \land F (P) = P) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K)$
43	14 42	eqtr4d	$⊢ (((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))) \land F (P) = P) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))$
44		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to (K \in HL \land W \in H)$
45		simpl2	$⊢ (((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))) \land F (P) \neq P) \to F \in T$
46		simpl31	$⊢ (((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))) \land F (P) \neq P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
47	1 2 3 4 5 6 7	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)) \underset{˙}{\land} W$
48	44 45 46 47	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W$
49		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to K \in HL$
50	49	hllatd	$⊢ (((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))) \land F (P) \neq P) \to K \in Lat$
51	20	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to P \in A$
52	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
53	44 45 51 52	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to F (P) \in A$
54		eqid	$⊢ {Base}_{K} = {Base}_{K}$
55	54 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land F (P) \in A) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
56	49 51 53 55	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to P \underset{˙}{\lor} F (P) \in {Base}_{K}$
57		simpl1r	$⊢ (((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))) \land F (P) \neq P) \to W \in H$
58	54 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
59	57 58	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to W \in {Base}_{K}$
60	54 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
61	50 56 59 60	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
62	48 61	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
63		simpl32	$⊢ (((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))) \land F (P) \neq P) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
64	1 2 3 4 5 6 7	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to R (F) = (Q \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W$
65	44 45 63 64	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to R (F) = (Q \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W$
66	34	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to Q \in A$
67	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$
68	44 45 66 67	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to F (Q) \in A$
69	54 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land F (Q) \in A) \to Q \underset{˙}{\lor} F (Q) \in {Base}_{K}$
70	49 66 68 69	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to Q \underset{˙}{\lor} F (Q) \in {Base}_{K}$
71	54 1 3	latmle1	$⊢ (K \in Lat \land Q \underset{˙}{\lor} F (Q) \in {Base}_{K} \land W \in {Base}_{K}) \to ((Q \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
72	50 70 59 71	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to ((Q \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
73	65 72	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
74	54 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
75	44 45 74	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to R (F) \in {Base}_{K}$
76	54 1 3	latlem12	$⊢ (K \in Lat \land (R (F) \in {Base}_{K} \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land Q \underset{˙}{\lor} F (Q) \in {Base}_{K})) \to ((R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))) \leftrightarrow R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))))$
77	50 75 56 70 76	syl13anc	$⊢ (((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))) \land F (P) \neq P) \to ((R (F) \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land R (F) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))) \leftrightarrow R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))))$
78	62 73 77	mpbi2and	$⊢ (((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))) \land F (P) \neq P) \to R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)))$
79	49 17	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to K \in AtLat$
80		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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to F (P) \neq P$
81	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$
82	44 46 45 80 81	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to R (F) \in A$
83	54 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} F (P) \in {Base}_{K} \land Q \underset{˙}{\lor} F (Q) \in {Base}_{K}) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in {Base}_{K}$
84	50 56 70 83	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in {Base}_{K}$
85	54 1 12 4	atlen0	$⊢ ((K \in AtLat \land (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in {Base}_{K} \land R (F) \in A) \land R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)))) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \neq 0. (K)$
86	79 84 82 78 85	syl31anc	$⊢ (((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))) \land F (P) \neq P) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \neq 0. (K)$
87	86	neneqd	$⊢ (((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))) \land F (P) \neq P) \to \neg (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K)$
88		simpl33	$⊢ (((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))) \land F (P) \neq P) \to P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q)$
89	2 3 12 4	2atmat0	$⊢ ((K \in HL \land P \in A \land F (P) \in A) \land (Q \in A \land F (Q) \in A \land P \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \to ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in A \lor (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K))$
90	49 51 53 66 68 88 89	syl33anc	$⊢ (((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))) \land F (P) \neq P) \to ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in A \lor (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K))$
91	90	ord	$⊢ (((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))) \land F (P) \neq P) \to (\neg (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in A \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) = 0. (K))$
92	87 91	mt3d	$⊢ (((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))) \land F (P) \neq P) \to (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in A$
93	1 4	atcmp	$⊢ (K \in AtLat \land R (F) \in A \land (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)) \in A) \to (R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))) \leftrightarrow R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)))$
94	79 82 92 93	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 \underset{˙}{\lor} F (P) \neq Q \underset{˙}{\lor} F (Q))) \land F (P) \neq P) \to (R (F) \underset{˙}{\leq} ((P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))) \leftrightarrow R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q)))$
95	78 94	mpbid	$⊢ (((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))) \land F (P) \neq P) \to R (F) = (P \underset{˙}{\lor} F (P)) \underset{˙}{\land} (Q \underset{˙}{\lor} F (Q))$
96	43 95	pm2.61dane	$⊢ ((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))$

Metamath Proof Explorer

Theorem trlval3

Proof