Theorem 3dimlem4OLDN

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

	Ref	Expression
Hypotheses	3dim0.j	⊢ ∨ = ( join ‘ 𝐾 )
	3dim0.l	⊢ ≤ = ( le ‘ 𝐾 )
	3dim0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	3dimlem4OLDN	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3dim0.j	⊢ ∨ = ( join ‘ 𝐾 )
2		3dim0.l	⊢ ≤ = ( le ‘ 𝐾 )
3		3dim0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → 𝑃 ≠ 𝑄 )
5		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
6		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
7		simp2l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
8		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
9		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝐴 )
10		simp3l	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ≠ 𝑅 )
11	10	necomd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ≠ 𝑄 )
12	2 1 3	hlatexch2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑄 ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
13	6 7 8 9 11 12	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
14	1 3	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑄 ) )
15	6 9 7 14	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑄 ) )
16	15	breq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ) )
17	13 16	sylibrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
18	17	3ad2ant1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
19	5 18	mtod	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
20		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) )
21		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
22	6 21	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ Lat )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24	23 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25	9 24	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
26	23 3	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
27	7 26	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
28	23 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
29	8 28	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
30	23 1	latjrot	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
31	22 25 27 29 30	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) = ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
32	31	breq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑆 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) ↔ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
33		simp2r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
34	23 1 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
35	6 9 7 34	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
36		simp3r	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
37	23 2 1 3	hlexch1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑆 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
38	6 33 8 35 36 37	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑆 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑃 ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
39	32 38	sylbird	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
40	39	3ad2ant1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) )
41	20 40	mtod	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
42	4 19 41	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑆 ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )