4atlem3a

Description: Lemma for 4at . Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem3a	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V))$

Proof

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4		simpl1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land P \in A \land Q \in A)$
5		simpl2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in A$
6		simpl2r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in A$
7		simpl12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in A$
8	5 6 7	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \in A \land S \in A \land P \in A)$
9		simpl3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (U \in A \land V \in A)$
10		simpr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
11	1 2 3	4atlem3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land P \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
12	4 8 9 10 11	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
13		simpl11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in HL$
14	13	hllatd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in Lat$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
17	7 16	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in {Base}_{K}$
18		simpl3l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to U \in A$
19		simpl3r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to V \in A$
20	15 2 3	hlatjcl	$⊢ (K \in HL \land U \in A \land V \in A) \to U \underset{˙}{\lor} V \in {Base}_{K}$
21	13 18 19 20	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to U \underset{˙}{\lor} V \in {Base}_{K}$
22	15 1 2	latlej1	$⊢ (K \in Lat \land P \in {Base}_{K} \land U \underset{˙}{\lor} V \in {Base}_{K}) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} (U \underset{˙}{\lor} V))$
23	14 17 21 22	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} (U \underset{˙}{\lor} V))$
24	15 3	atbase	$⊢ U \in A \to U \in {Base}_{K}$
25	18 24	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to U \in {Base}_{K}$
26	15 3	atbase	$⊢ V \in A \to V \in {Base}_{K}$
27	19 26	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to V \in {Base}_{K}$
28	15 2	latjass	$⊢ (K \in Lat \land (P \in {Base}_{K} \land U \in {Base}_{K} \land V \in {Base}_{K})) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} V = P \underset{˙}{\lor} (U \underset{˙}{\lor} V)$
29	14 17 25 27 28	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} V = P \underset{˙}{\lor} (U \underset{˙}{\lor} V)$
30	23 29	breqtrrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)$
31		biortn	$⊢ P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \leftrightarrow (\neg P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
32	30 31	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \leftrightarrow (\neg P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
33	32	orbi1d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V))) \leftrightarrow ((\neg P \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \lor (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V))))$
34	12 33	mpbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
35		3orass	$⊢ (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)) \leftrightarrow (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor (\neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V)))$
36	34 35	sylibr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (U \in A \land V \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} U) \underset{˙}{\lor} V))$

Metamath Proof Explorer

Theorem 4atlem3a

Proof