cdlemg2m

	Ref	Expression
Hypotheses	cdlemg2inv.h	$⊢ H = LHyp (K)$
	cdlemg2inv.t	$⊢ T = LTrn (K) (W)$
	cdlemg2j.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemg2j.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemg2j.a	$⊢ A = Atoms (K)$
	cdlemg2j.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemg2j.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
Assertion	cdlemg2m	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W = U$

Proof

Step	Hyp	Ref	Expression
1		cdlemg2inv.h	$⊢ H = LHyp (K)$
2		cdlemg2inv.t	$⊢ T = LTrn (K) (W)$
3		cdlemg2j.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4		cdlemg2j.j	$⊢ \underset{˙}{\lor} = join (K)$
5		cdlemg2j.a	$⊢ A = Atoms (K)$
6		cdlemg2j.m	$⊢ \underset{˙}{\land} = meet (K)$
7		cdlemg2j.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8	1 2 3 4 5 6 7	cdlemg2k	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to F (P) \underset{˙}{\lor} F (Q) = F (P) \underset{˙}{\lor} U$
9	8	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W = (F (P) \underset{˙}{\lor} U) \underset{˙}{\land} W$
10		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (K \in HL \land W \in H)$
11		simp3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to F \in T$
12		simp2l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
13		eqid	$⊢ 0. (K) = 0. (K)$
14	3 6 13 5 1 2	ltrnmw	$⊢ ((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{˙}{\land} W = 0. (K)$
15	10 11 12 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to F (P) \underset{˙}{\land} W = 0. (K)$
16	15	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} U = 0. (K) \underset{˙}{\lor} U$
17		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to K \in HL$
18	3 5 1 2	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)$
19	10 11 12 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
20	19	simpld	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to F (P) \in A$
21		simp1r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to W \in H$
22		simp2ll	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to P \in A$
23		simp2rl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to Q \in A$
24		eqid	$⊢ {Base}_{K} = {Base}_{K}$
25	3 4 6 5 1 7 24	cdleme0aa	$⊢ ((K \in HL \land W \in H) \land P \in A \land Q \in A) \to U \in {Base}_{K}$
26	17 21 22 23 25	syl211anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to U \in {Base}_{K}$
27	24 1	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
28	21 27	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to W \in {Base}_{K}$
29	17	hllatd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to K \in Lat$
30	24 4 5	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
31	17 22 23 30	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
32	24 3 6	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
33	29 31 28 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
34	7 33	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to U \underset{˙}{\leq} W$
35	24 3 4 6 5	atmod4i2	$⊢ (K \in HL \land (F (P) \in A \land U \in {Base}_{K} \land W \in {Base}_{K}) \land U \underset{˙}{\leq} W) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} U = (F (P) \underset{˙}{\lor} U) \underset{˙}{\land} W$
36	17 20 26 28 34 35	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \underset{˙}{\land} W) \underset{˙}{\lor} U = (F (P) \underset{˙}{\lor} U) \underset{˙}{\land} W$
37		hlol	$⊢ K \in HL \to K \in OL$
38	17 37	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to K \in OL$
39	24 4 13	olj02	$⊢ (K \in OL \land U \in {Base}_{K}) \to 0. (K) \underset{˙}{\lor} U = U$
40	38 26 39	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to 0. (K) \underset{˙}{\lor} U = U$
41	16 36 40	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \underset{˙}{\lor} U) \underset{˙}{\land} W = U$
42	9 41	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land F \in T) \to (F (P) \underset{˙}{\lor} F (Q)) \underset{˙}{\land} W = U$

Metamath Proof Explorer

Theorem cdlemg2m

Proof