cdlemc6

	Ref	Expression
Hypotheses	cdlemc3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemc3.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemc3.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemc3.a	$⊢ A = Atoms (K)$
	cdlemc3.h	$⊢ H = LHyp (K)$
	cdlemc3.t	$⊢ T = LTrn (K) (W)$
	cdlemc3.r	$⊢ R = trL (K) (W)$
Assertion	cdlemc6	$⊢ ((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 F (P) = P) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$

Proof

Step	Hyp	Ref	Expression
1		cdlemc3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemc3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemc3.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemc3.a	$⊢ A = Atoms (K)$
5		cdlemc3.h	$⊢ H = LHyp (K)$
6		cdlemc3.t	$⊢ T = LTrn (K) (W)$
7		cdlemc3.r	$⊢ R = trL (K) (W)$
8		simp1l	$⊢ ((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 F (P) = P) \to K \in HL$
9		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 F (P) = P) \to P \in A$
10		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 F (P) = P) \to Q \in A$
11	2 4	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
12	8 9 10 11	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 F (P) = P) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
13	12	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 F (P) = P) \to Q \underset{˙}{\land} (P \underset{˙}{\lor} Q) = Q \underset{˙}{\land} (Q \underset{˙}{\lor} P)$
14	8	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 F (P) = P) \to K \in Lat$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
17	10 16	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 F (P) = P) \to Q \in {Base}_{K}$
18	15 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
19	9 18	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 F (P) = P) \to P \in {Base}_{K}$
20	15 2 3	latabs2	$⊢ (K \in Lat \land Q \in {Base}_{K} \land P \in {Base}_{K}) \to Q \underset{˙}{\land} (Q \underset{˙}{\lor} P) = Q$
21	14 17 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 F (P) = P) \to Q \underset{˙}{\land} (Q \underset{˙}{\lor} P) = Q$
22	13 21	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 F (P) = P) \to Q \underset{˙}{\land} (P \underset{˙}{\lor} Q) = Q$
23		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 F (P) = P) \to (K \in HL \land W \in H)$
24		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 F (P) = P) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
25		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 F (P) = P) \to F \in T$
26		simp3	$⊢ ((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 F (P) = P) \to F (P) = P$
27		eqid	$⊢ 0. (K) = 0. (K)$
28	1 27 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)$
29	23 24 25 26 28	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 F (P) = P) \to R (F) = 0. (K)$
30	29	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 F (P) = P) \to Q \underset{˙}{\lor} R (F) = Q \underset{˙}{\lor} 0. (K)$
31		hlol	$⊢ K \in HL \to K \in OL$
32	8 31	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 F (P) = P) \to K \in OL$
33	15 2 27	olj01	$⊢ (K \in OL \land Q \in {Base}_{K}) \to Q \underset{˙}{\lor} 0. (K) = Q$
34	32 17 33	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 F (P) = P) \to Q \underset{˙}{\lor} 0. (K) = Q$
35	30 34	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 F (P) = P) \to Q \underset{˙}{\lor} R (F) = Q$
36	26	oveq1d	$⊢ ((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 F (P) = P) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
37	15 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
38	8 9 10 37	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 F (P) = P) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
39		simp1r	$⊢ ((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 F (P) = P) \to W \in H$
40	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
41	39 40	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 F (P) = P) \to W \in {Base}_{K}$
42	15 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
43	14 38 41 42	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 F (P) = P) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
44	15 2	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} P$
45	14 19 43 44	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 F (P) = P) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} P$
46	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
47	8 9 10 46	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 F (P) = P) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
48	15 1 2 3 4	atmod2i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (W \underset{˙}{\lor} P)$
49	8 9 38 41 47 48	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 F (P) = P) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (W \underset{˙}{\lor} P)$
50		eqid	$⊢ 1. (K) = 1. (K)$
51	1 2 50 4 5	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)$
52	8 39 24 51	syl21anc	$⊢ ((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 F (P) = P) \to W \underset{˙}{\lor} P = 1. (K)$
53	52	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 F (P) = P) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (W \underset{˙}{\lor} P) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K)$
54	15 3 50	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
55	32 38 54	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 F (P) = P) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
56	49 53 55	3eqtrd	$⊢ ((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 F (P) = P) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
57	36 45 56	3eqtrd	$⊢ ((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 F (P) = P) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} Q$
58	35 57	oveq12d	$⊢ ((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 F (P) = P) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) = Q \underset{˙}{\land} (P \underset{˙}{\lor} Q)$
59	1 4 5 6	ltrnateq	$⊢ ((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 F (P) = P) \to F (Q) = Q$
60	22 58 59	3eqtr4rd	$⊢ ((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 F (P) = P) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$

Metamath Proof Explorer

Theorem cdlemc6

Proof