cdlemg31b

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemg12.a	$⊢ A = Atoms (K)$
5		cdlemg12.h	$⊢ H = LHyp (K)$
6		cdlemg12.t	$⊢ T = LTrn (K) (W)$
7		cdlemg12b.r	$⊢ R = trL (K) (W)$
8		cdlemg31.n	$⊢ N = (P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))$
9		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to K \in HL$
10	9	hllatd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to K \in Lat$
11		simp2l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to P \in A$
12		simp3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to v \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land v \in A) \to P \underset{˙}{\lor} v \in {Base}_{K}$
15	9 11 12 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to P \underset{˙}{\lor} v \in {Base}_{K}$
16		simp2r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to Q \in A$
17	13 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to Q \in {Base}_{K}$
19		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to (K \in HL \land W \in H)$
20		simp3r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to F \in T$
21	13 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
22	19 20 21	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to R (F) \in {Base}_{K}$
23	13 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R (F) \in {Base}_{K}) \to Q \underset{˙}{\lor} R (F) \in {Base}_{K}$
24	10 18 22 23	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to Q \underset{˙}{\lor} R (F) \in {Base}_{K}$
25	13 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} v \in {Base}_{K} \land Q \underset{˙}{\lor} R (F) \in {Base}_{K}) \to ((P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$
26	10 15 24 25	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to ((P \underset{˙}{\lor} v) \underset{˙}{\land} (Q \underset{˙}{\lor} R (F))) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$
27	8 26	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A) \land (v \in A \land F \in T)) \to N \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$

Metamath Proof Explorer

Theorem cdlemg31b

Proof