Theorem 4atlem12a

Description: Lemma for 4at . Substitute T for P . (Contributed by NM, 9-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	⊢ ≤ = ( le ‘ 𝐾 )
	4at.j	⊢ ∨ = ( join ‘ 𝐾 )
	4at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	4atlem12a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		4at.l	⊢ ≤ = ( le ‘ 𝐾 )
2		4at.j	⊢ ∨ = ( join ‘ 𝐾 )
3		4at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simp11	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝐾 ∈ HL )
5		simp12	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
6		simp13	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑇 ∈ 𝐴 )
7	4	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝐾 ∈ Lat )
8		simp21	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑈 ∈ 𝐴 )
9		simp22	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑉 ∈ 𝐴 )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11	10 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
12	4 8 9 11	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
13		simp23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑊 ∈ 𝐴 )
14	10 3	atbase	⊢ ( 𝑊 ∈ 𝐴 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
15	13 14	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
16	10 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
17	7 12 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
18		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) )
19	10 1 2 3	hlexchb2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ↔ ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) )
20	4 5 6 17 18 19	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ↔ ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) )
21	1 2 3	4atlem4a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) )
22	4 6 8 9 13 21	syl32anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) )
23	22	breq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ 𝑃 ≤ ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) )
24	1 2 3	4atlem4a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) )
25	4 5 8 9 13 24	syl32anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) )
26	25 22	eqeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( 𝑃 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) = ( 𝑇 ∨ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) ) )
27	20 23 26	3bitr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑃 ≤ ( ( 𝑈 ∨ 𝑉 ) ∨ 𝑊 ) ) → ( 𝑃 ≤ ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) = ( ( 𝑇 ∨ 𝑈 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )