This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( 𝑞 = 𝑟 → 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) ) )
18 17 necon3bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → ( ¬ 𝑟 ∈ ( 𝑋 ∩ ( ⊥ ‘ 𝑋 ) ) → 𝑞 ≠ 𝑟 ) )
19 10 18 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘ 𝑋 ) ) ) → 𝑞 ≠ 𝑟 )