Theorem 4atlem10b

Description: Lemma for 4at . Substitute V for R (cont.). (Contributed by NM, 10-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	⊢ ≤ = ( le ‘ 𝐾 )
	4at.j	⊢ ∨ = ( join ‘ 𝐾 )
	4at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	4atlem10b	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		4at.l	⊢ ≤ = ( le ‘ 𝐾 )
2		4at.j	⊢ ∨ = ( join ‘ 𝐾 )
3		4at.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simprr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
5		simprl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
6		simpl1	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) )
7		simpl21	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑅 ∈ 𝐴 )
8		simpl23	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑉 ∈ 𝐴 )
9		simpl31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑊 ∈ 𝐴 )
10		simpl32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) )
11	1 2 3	4atlem10a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ) → ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
12	6 7 8 9 10 11	syl131anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) )
13	5 12	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )
14	4 13	breqtrrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) )
15		simpl22	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → 𝑆 ∈ 𝐴 )
16		simpl33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
17	1 2 3	4atlem9	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ) )
18	6 7 15 9 16 17	syl131anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) ) )
19	14 18	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑊 ) ) )
20	19 13	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑊 ) ∧ ¬ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ∧ ( 𝑅 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ∧ 𝑆 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑅 ∨ 𝑆 ) ) = ( ( 𝑃 ∨ 𝑄 ) ∨ ( 𝑉 ∨ 𝑊 ) ) )