Theorem atcvrneN

Description: Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		atcvrne.j	⊢ ∨ = ( join ‘ 𝐾 )
2		atcvrne.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		atcvrne.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
5	4	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ AtLat )
6		simp21	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
7		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
8	7 3	atn0	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ ( 0. ‘ 𝐾 ) )
9	5 6 8	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≠ ( 0. ‘ 𝐾 ) )
10		simp1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13	6 12	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
14		simp22	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
15		simp23	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
16		simp3	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )
17	11 1 7 2 3	atcvrj0	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 = ( 0. ‘ 𝐾 ) ↔ 𝑄 = 𝑅 ) )
18	10 13 14 15 16 17	syl131anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 = ( 0. ‘ 𝐾 ) ↔ 𝑄 = 𝑅 ) )
19	18	necon3bid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 ≠ ( 0. ‘ 𝐾 ) ↔ 𝑄 ≠ 𝑅 ) )
20	9 19	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ≠ 𝑅 )