cdlemg2kq

Description: cdlemg2k with P and Q swapped. TODO: FIX COMMENT. (Contributed by NM, 15-May-2013)

	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	cdlemg2kq	$⊢ ((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 (Q) \underset{˙}{\lor} 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		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)$
9		simp2r	$⊢ ((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 \land \neg Q \underset{˙}{\leq} W)$
10		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)$
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		eqid	$⊢ (Q \underset{˙}{\lor} P) \underset{˙}{\land} W = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
13	1 2 3 4 5 6 12	cdlemg2k	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land F \in T) \to F (Q) \underset{˙}{\lor} F (P) = F (Q) \underset{˙}{\lor} ((Q \underset{˙}{\lor} P) \underset{˙}{\land} W)$
14	8 9 10 11 13	syl121anc	$⊢ ((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 (Q) \underset{˙}{\lor} F (P) = F (Q) \underset{˙}{\lor} ((Q \underset{˙}{\lor} P) \underset{˙}{\land} W)$
15		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$
16		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$
17	3 5 1 2	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
18	8 11 16 17	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$
19		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$
20	3 5 1 2	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in A) \to F (Q) \in A$
21	8 11 19 20	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 (Q) \in A$
22	4 5	hlatjcom	$⊢ (K \in HL \land F (P) \in A \land F (Q) \in A) \to F (P) \underset{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} F (P)$
23	15 18 21 22	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{˙}{\lor} F (Q) = F (Q) \underset{˙}{\lor} F (P)$
24	4 5	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
25	15 16 19 24	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 = Q \underset{˙}{\lor} P$
26	25	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 (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
27	7 26	syl5eq	$⊢ ((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 = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
28	27	oveq2d	$⊢ ((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 (Q) \underset{˙}{\lor} U = F (Q) \underset{˙}{\lor} ((Q \underset{˙}{\lor} P) \underset{˙}{\land} W)$
29	14 23 28	3eqtr4d	$⊢ ((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 (Q) \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem cdlemg2kq

Proof