4atlem10

Description: Lemma for 4at . Combine both possible 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	4atlem10	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

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		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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$
5	4	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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$
6		simp21l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
9	6 8	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 {Base}_{K}$
10		simp21r	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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$
11	7 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
12	10 11	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 {Base}_{K}$
13	7 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
14	13	3ad2ant1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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} Q \in {Base}_{K}$
15		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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$
16		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 W \in A$
17	7 2 3	hlatjcl	$⊢ (K \in HL \land V \in A \land W \in A) \to V \underset{˙}{\lor} W \in {Base}_{K}$
18	4 15 16 17	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \underset{˙}{\lor} W \in {Base}_{K}$
19	7 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land V \underset{˙}{\lor} W \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
20	5 14 18 19	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
21	7 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land S \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
22	5 9 12 20 21	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
23		simp11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (K \in HL \land P \in A \land Q \in A)$
24	6 10 15	3jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 V \in A)$
25	24	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (R \in A \land S \in A \land V \in A)$
26	16	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to W \in A$
27		simp2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W)$
28		simp33	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
29	28	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
30	26 27 29	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (W \in A \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
31		simp3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
32	1 2 3	4atlem10b	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land V \in A) \land (W \in A \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
33	23 25 30 31 32	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
34	33	3exp	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \to ((R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
35	2 3	hlatjcom	$⊢ (K \in HL \land S \in A \land R \in A) \to S \underset{˙}{\lor} R = R \underset{˙}{\lor} S$
36	4 10 6 35	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \underset{˙}{\lor} R = R \underset{˙}{\lor} S$
37	36	oveq2d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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} Q) \underset{˙}{\lor} (S \underset{˙}{\lor} R) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
38	37	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (S \underset{˙}{\lor} R) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
39		simp11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (K \in HL \land P \in A \land Q \in A)$
40	10 6 15	3jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \land R \in A \land V \in A)$
41	40	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (S \in A \land R \in A \land V \in A)$
42	16	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to W \in A$
43		simp2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W)$
44		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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$
45		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 Q \in A$
46	44 45	jca	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \land Q \in A)$
47		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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)$
48		simp32	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
49	1 2 3	4atlem0a	$⊢ ((K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \in A)) \land (\neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)$
50	4 46 47 48 28 49	syl32anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)$
51	50	3ad2ant1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S)$
52	42 43 51	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (W \in A \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S))$
53		simprr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
54		simprl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
55	53 54	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
56	55	3adant2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
57	1 2 3	4atlem10b	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (S \in A \land R \in A \land V \in A) \land (W \in A \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land \neg R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} S))) \land (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (S \underset{˙}{\lor} R) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
58	39 41 52 56 57	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (S \underset{˙}{\lor} R) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
59	38 58	eqtr3d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \land (R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
60	59	3exp	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \to ((R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
61		simp1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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)$
62		simp3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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))$
63	1 2 3	4atlem3b	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \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 R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W))$
64	61 6 10 16 62 63	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 R \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} W))$
65	34 60 64	mpjaod	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
66	22 65	sylbird	$⊢ ((K \in HL \land P \in A \land Q \in A) \land ((R \in A \land S \in A) \land V \in A \land W \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 \underset{˙}{\lor} S) \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Metamath Proof Explorer

Theorem 4atlem10

Proof