3dimlem3OLDN

Description: Lemma for 3dim1 . (Contributed by NM, 25-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
	3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	3dim0.a	$⊢ A = Atoms (K)$
Assertion	3dimlem3OLDN	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	$⊢ \underset{˙}{\lor} = join (K)$
2		3dim0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		3dim0.a	$⊢ A = Atoms (K)$
4		simpr1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to P \neq Q$
5		simpr2	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
6		simpl11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to K \in HL$
7		simpl2l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to R \in A$
8		simpl12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to P \in A$
9		simpl13	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to Q \in A$
10		simpl3l	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to Q \neq R$
11	10	necomd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to R \neq Q$
12	2 1 3	hlatexch2	$⊢ (K \in HL \land (R \in A \land P \in A \land Q \in A) \land R \neq Q) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
13	6 7 8 9 11 12	syl131anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
14	1 3	hlatjcom	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
15	6 9 7 14	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
16	15	breq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
17	13 16	sylibrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))$
18	5 17	mtod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
19		simpl3r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
20		hllat	$⊢ K \in HL \to K \in Lat$
21	6 20	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to K \in Lat$
22		eqid	$⊢ {Base}_{K} = {Base}_{K}$
23	22 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
24	9 23	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to Q \in {Base}_{K}$
25	22 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
26	7 25	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to R \in {Base}_{K}$
27	22 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
28	8 27	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to P \in {Base}_{K}$
29	22 1	latjrot	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \in {Base}_{K} \land P \in {Base}_{K})) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
30	21 24 26 28 29	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
31		simpr3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
32		simpl2r	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to S \in A$
33	22 1 3	hlatjcl	$⊢ (K \in HL \land Q \in A \land R \in A) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
34	6 9 7 33	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
35	22 2 1 3	hlexchb1	$⊢ (K \in HL \land (P \in A \land S \in A \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to (P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
36	6 8 32 34 5 35	syl131anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S) \leftrightarrow (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
37	31 36	mpbid	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} P = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
38	30 37	eqtr3d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S$
39	38	breq2d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) \leftrightarrow T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
40	19 39	mtbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to \neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
41	4 18 40	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (Q \neq R \land \neg T \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \land (P \neq Q \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$

Metamath Proof Explorer

Theorem 3dimlem3OLDN

Proof