Theorem atexchltN

Description: Atom exchange property. Version of hlatexch2 with less-than ordering. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atexchlt.s	⊢ < = ( lt ‘ 𝐾 )
	atexchlt.j	⊢ ∨ = ( join ‘ 𝐾 )
	atexchlt.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atexchltN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 < ( 𝑄 ∨ 𝑅 ) → 𝑄 < ( 𝑃 ∨ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		atexchlt.s	⊢ < = ( lt ‘ 𝐾 )
2		atexchlt.j	⊢ ∨ = ( join ‘ 𝐾 )
3		atexchlt.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
5	2 3 4	atexchcvrN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) → 𝑄 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
6	1 2 3 4	atltcvr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑃 < ( 𝑄 ∨ 𝑅 ) ↔ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
7	6	3adant3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 < ( 𝑄 ∨ 𝑅 ) ↔ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
8		simpl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
9		simpr2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
10		simpr1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
11		simpr3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
12	1 2 3 4	atltcvr	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑄 < ( 𝑃 ∨ 𝑅 ) ↔ 𝑄 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
13	8 9 10 11 12	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑄 < ( 𝑃 ∨ 𝑅 ) ↔ 𝑄 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
14	13	3adant3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑄 < ( 𝑃 ∨ 𝑅 ) ↔ 𝑄 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
15	5 7 14	3imtr4d	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 < ( 𝑄 ∨ 𝑅 ) → 𝑄 < ( 𝑃 ∨ 𝑅 ) ) )