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

Metamath Proof Explorer

Theorem osumcllem4N

Description: Lemma for osumclN . (Contributed by NM, 24-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcllem.l ⊢ ≤ = ( le ‘ 𝐾 )
osumcllem.j ⊢ ∨ = ( join ‘ 𝐾 )
osumcllem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
osumcllem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
osumcllem.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
osumcllem.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
osumcllem.m ⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
osumcllem.u ⊢ 𝑈 = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
Assertion osumcllem4N ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → 𝑞 ≠ 𝑟 )

Proof

Step Hyp Ref Expression
1 osumcllem.l ⊢ ≤ = ( le ‘ 𝐾 )
2 osumcllem.j ⊢ ∨ = ( join ‘ 𝐾 )
3 osumcllem.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 osumcllem.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 osumcllem.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
6 osumcllem.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
7 osumcllem.m ⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
8 osumcllem.u ⊢ 𝑈 = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
9 n0i ⊢ ( 𝑟 ∈ ( 𝑋 ∩ 𝑌 ) → ¬ ( 𝑋 ∩ 𝑌 ) = ∅ )
10 incom ⊢ ( 𝑋 ∩ 𝑌 ) = ( 𝑌 ∩ 𝑋 )
11 sslin ⊢ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) → ( 𝑌 ∩ 𝑋 ) ⊆ ( 𝑌 ∩ ( ⊥ ‘ 𝑌 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑌 ∩ 𝑋 ) ⊆ ( 𝑌 ∩ ( ⊥ ‘ 𝑌 ) ) )
13 10 12 eqsstrid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 ∩ 𝑌 ) ⊆ ( 𝑌 ∩ ( ⊥ ‘ 𝑌 ) ) )
14 3 5 pnonsingN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 ∩ ( ⊥ ‘ 𝑌 ) ) = ∅ )
15 14 3adant3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑌 ∩ ( ⊥ ‘ 𝑌 ) ) = ∅ )
16 13 15 sseqtrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 ∩ 𝑌 ) ⊆ ∅ )
17 ss0b ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ ∅ ↔ ( 𝑋 ∩ 𝑌 ) = ∅ )
18 16 17 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) → ( 𝑋 ∩ 𝑌 ) = ∅ )
19 18 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → ( 𝑋 ∩ 𝑌 ) = ∅ )
20 9 19 nsyl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → ¬ 𝑟 ∈ ( 𝑋 ∩ 𝑌 ) )
21 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → 𝑞 ∈ 𝑌 )
22 eleq1w ⊢ ( 𝑞 = 𝑟 → ( 𝑞 ∈ 𝑌 ↔ 𝑟 ∈ 𝑌 ) )
23 21 22 syl5ibcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → ( 𝑞 = 𝑟 → 𝑟 ∈ 𝑌 ) )
24 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → 𝑟 ∈ 𝑋 )
25 23 24 jctild ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → ( 𝑞 = 𝑟 → ( 𝑟 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) ) )
26 elin ⊢ ( 𝑟 ∈ ( 𝑋 ∩ 𝑌 ) ↔ ( 𝑟 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ) )
27 25 26 imbitrrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → ( 𝑞 = 𝑟 → 𝑟 ∈ ( 𝑋 ∩ 𝑌 ) ) )
28 27 necon3bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → ( ¬ 𝑟 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑞 ≠ 𝑟 ) )
29 20 28 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ) ∧ ( 𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ) ) → 𝑞 ≠ 𝑟 )