Theorem pexmidlem1N

Description: Lemma for pexmidN . Holland's proof implicitly requires q =/= r , which we prove here. (Contributed by NM, 2-Feb-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pexmidlem.l	⊢ ≤ = ( le ‘ 𝐾 )
	pexmidlem.j	⊢ ∨ = ( join ‘ 𝐾 )
	pexmidlem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pexmidlem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
	pexmidlem.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
	pexmidlem.m	⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
Assertion	pexmidlem1N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → 𝑞 ≠ 𝑟 )

Proof

Step	Hyp	Ref	Expression
1		pexmidlem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		pexmidlem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		pexmidlem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		pexmidlem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
5		pexmidlem.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
6		pexmidlem.m	⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
7		n0i	⊢ ( 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) → ¬ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = ∅ )
8	3 5	pnonsingN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = ∅ )
9	8	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) = ∅ )
10	7 9	nsyl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ¬ 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) )
11		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → 𝑞 ∈ ( ⊥ ‘ 𝑋 ) )
12		eleq1w	⊢ ( 𝑞 = 𝑟 → ( 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ↔ 𝑟 ∈ ( ⊥ ‘ 𝑋 ) ) )
13	11 12	syl5ibcom	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑞 = 𝑟 → 𝑟 ∈ ( ⊥ ‘ 𝑋 ) ) )
14		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → 𝑟 ∈ 𝑋 )
15	13 14	jctild	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑞 = 𝑟 → ( 𝑟 ∈ 𝑋 ∧ 𝑟 ∈ ( ⊥ ‘ 𝑋 ) ) ) )
16		elin	⊢ ( 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ↔ ( 𝑟 ∈ 𝑋 ∧ 𝑟 ∈ ( ⊥ ‘ 𝑋 ) ) )
17	15 16	syl6ibr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑞 = 𝑟 → 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ) )
18	17	necon3bd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( ¬ 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) → 𝑞 ≠ 𝑟 ) )
19	10 18	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → 𝑞 ≠ 𝑟 )