Theorem cvrat42

Description: Commuted version of cvrat4 . (Contributed by NM, 28-Jan-2012)

	Ref	Expression
Hypotheses	cvrat4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrat4.l	⊢ ≤ = ( le ‘ 𝐾 )
	cvrat4.j	⊢ ∨ = ( join ‘ 𝐾 )
	cvrat4.z	⊢ 0 = ( 0. ‘ 𝐾 )
	cvrat4.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	cvrat42	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvrat4.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrat4.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cvrat4.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cvrat4.z	⊢ 0 = ( 0. ‘ 𝐾 )
5		cvrat4.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6	1 2 3 4 5	cvrat4	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
7		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8	7	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ Lat )
9		simplr3	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
10	1 5	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
11	9 10	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ∈ 𝐵 )
12	1 5	atbase	⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵 )
13	12	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐵 )
14	1 3	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( 𝑄 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑄 ) )
15	8 11 13 14	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑄 ) )
16	15	breq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) )
17	16	anbi2d	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ↔ ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) ) )
18	17	rexbidva	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) ) )
19	6 18	sylibd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) ) )