This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dalawlem14

Description: Lemma for dalaw . Combine dalawlem10 and dalawlem13 . (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	dalawlem14	$⊢ ((K \in HL \land \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P))) \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		ianor	$⊢ \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P))) \leftrightarrow (\neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \lor \neg (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P)))$
7	1 2 3 4 5	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)))$
8	7	3expib	$⊢ (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)) \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))))$
9	8	3exp	$⊢ K \in HL \to (\neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \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))))))$
10	1 2 3 4	dalawlem10	$⊢ ((K \in HL \land \neg (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \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)))$
11	10	3expib	$⊢ (K \in HL \land \neg (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \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))))$
12	11	3exp	$⊢ K \in HL \to (\neg (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \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))))))$
13	9 12	jaod	$⊢ K \in HL \to ((\neg (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \lor \neg (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P))) \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))))))$
14	6 13	biimtrid	$⊢ K \in HL \to (\neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P))) \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))))))$
15	14	3imp	$⊢ (K \in HL \land \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P))) \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))))$
16	15	3impib	$⊢ ((K \in HL \land \neg ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in O \land (\neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} T)) \underset{˙}{\leq} (R \underset{˙}{\lor} P))) \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)))$