dalawlem13

Description: Lemma for dalaw . Special case to eliminate the requirement ( ( P .\/ Q ) .\/ R ) e. O in dalawlem1 . (Contributed by NM, 6-Oct-2012)

	Ref	Expression
Hypotheses	dalawlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalawlem.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalawlem.m	$⊢ \underset{˙}{\land} = meet (K)$
	dalawlem.a	$⊢ A = Atoms (K)$
	dalawlem2.o	$⊢ O = LPlanes (K)$
Assertion	dalawlem13	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$

Proof

Step	Hyp	Ref	Expression
1		dalawlem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dalawlem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dalawlem.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dalawlem.a	$⊢ A = Atoms (K)$
5		dalawlem2.o	$⊢ O = LPlanes (K)$
6		simp11	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to K \in HL$
7		simp12	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O$
8		simp22	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to Q \in A$
9		simp23	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to R \in A$
10		simp21	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to P \in A$
11	1 2 4 5	islpln2a	$⊢ (K \in HL \land (Q \in A \land R \in A \land P \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} P \in O \leftrightarrow (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
12	6 8 9 10 11	syl13anc	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} P \in O \leftrightarrow (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
13		df-ne	$⊢ Q \neq R \leftrightarrow \neg Q = R$
14	13	anbi1i	$⊢ (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (\neg Q = R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
15		pm4.56	$⊢ (\neg Q = R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow \neg (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
16	14 15	bitri	$⊢ (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow \neg (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
17	12 16	bitr2di	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (\neg (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P \in O)$
18	2 4	hlatjrot	$⊢ (K \in HL \land (Q \in A \land R \in A \land P \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
19	6 8 9 10 18	syl13anc	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
20	19	eleq1d	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} P \in O \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O)$
21	17 20	bitrd	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (\neg (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O)$
22	21	con1bid	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (\neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \leftrightarrow (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)))$
23	7 22	mpbid	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
24		simp13	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
25		simp2	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (P \in A \land Q \in A \land R \in A)$
26		simp3	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to (S \in A \land T \in A \land U \in A)$
27	1 2 3 4	dalawlem12	$⊢ ((K \in HL \land Q = R \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
28	27	3expib	$⊢ (K \in HL \land Q = R \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \to (((P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))$
29	28	3exp	$⊢ K \in HL \to (Q = R \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U) \to (((P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))))$
30	1 2 3 4	dalawlem11	$⊢ ((K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
31	30	3expib	$⊢ (K \in HL \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \to (((P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))$
32	31	3exp	$⊢ K \in HL \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U) \to (((P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))))$
33	29 32	jaod	$⊢ K \in HL \to ((Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U) \to (((P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))))$
34	33	3imp	$⊢ (K \in HL \land (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \to (((P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S))))$
35	34	3impib	$⊢ ((K \in HL \land (Q = R \lor P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$
36	6 23 24 25 26 35	syl311anc	$⊢ ((K \in HL \land \neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (S \underset{˙}{\lor} T)) \underset{˙}{\leq} (((Q \underset{˙}{\lor} R) \underset{˙}{\land} (T \underset{˙}{\lor} U)) \underset{˙}{\lor} ((R \underset{˙}{\lor} P) \underset{˙}{\land} (U \underset{˙}{\lor} S)))$

Metamath Proof Explorer

Theorem dalawlem13

Proof