Theorem atexchcvrN

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

	Ref	Expression
Hypotheses	atexchcvr.j	⊢ ∨ = ( join ‘ 𝐾 )
	atexchcvr.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	atexchcvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	atexchcvrN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		atexchcvr.j	⊢ ∨ = ( join ‘ 𝐾 )
2		atexchcvr.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3		atexchcvr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
5		simpl21	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
6		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7	6 2	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
8	5 7	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
9	4	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ Lat )
10		simpl22	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
11	6 2	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12	10 11	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13		simpl23	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
14	6 2	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
15	13 14	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
16	6 1	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
17	9 12 15 16	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
18	4 8 17	3jca	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
19		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
20	6 19 3	cvrle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
21	18 20	sylancom	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
22	21	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
23	19 1 2	hlatexch2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) )
24		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
25		simpl22	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
26		simpl21	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
27		simpl23	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
28		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑃 ≠ 𝑅 )
29		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) )
30	19 1 3 2	atcvrj2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) )
31	24 25 26 27 28 29 30	syl132anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) )
32	31	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑅 ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) ) )
33	22 23 32	3syld	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → 𝑄 𝐶 ( 𝑃 ∨ 𝑅 ) ) )