Theorem llnexch2N

Description: Line exchange property (compare cvlatexch2 for atoms). (Contributed by NM, 18-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	llnexch.l	⊢ ≤ = ( le ‘ 𝐾 )
	llnexch.j	⊢ ∨ = ( join ‘ 𝐾 )
	llnexch.m	⊢ ∧ = ( meet ‘ 𝐾 )
	llnexch.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	llnexch.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
Assertion	llnexch2N	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 → ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		llnexch.l	⊢ ≤ = ( le ‘ 𝐾 )
2		llnexch.j	⊢ ∨ = ( join ‘ 𝐾 )
3		llnexch.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		llnexch.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		llnexch.n	⊢ 𝑁 = ( LLines ‘ 𝐾 )
6	1 2 3 4 5	llnexchb2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 ↔ ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) ) )
7		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
8	7	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝐾 ∈ Lat )
9		simp21	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑋 ∈ 𝑁 )
10		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11	10 5	llnbase	⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
12	9 11	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
13		simp22	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑌 ∈ 𝑁 )
14	10 5	llnbase	⊢ ( 𝑌 ∈ 𝑁 → 𝑌 ∈ ( Base ‘ 𝐾 ) )
15	13 14	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → 𝑌 ∈ ( Base ‘ 𝐾 ) )
16	10 1 3	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
17	8 12 15 16	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 )
18		breq1	⊢ ( ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )
19	17 18	syl5ibcom	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) = ( 𝑋 ∧ 𝑍 ) → ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )
20	6 19	sylbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍 ) ) → ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑍 → ( 𝑋 ∧ 𝑍 ) ≤ 𝑌 ) )