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

Metamath Proof Explorer

Theorem osumcllem11N

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

Ref Expression
Hypotheses osumcl.p ⊢ + = ( +𝑃 ‘ 𝐾 )
osumcl.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
osumcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
Assertion osumcllem11N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 osumcl.p ⊢ + = ( +𝑃 ‘ 𝐾 )
2 osumcl.o ⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3 osumcl.c ⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
4 nonconne ⊢ ¬ ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 )
5 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → 𝐾 ∈ HL )
6 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ∈ 𝐶 )
7 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 7 3 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
9 5 6 8 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
10 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → 𝑌 ∈ 𝐶 )
11 7 3 psubclssatN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
12 5 10 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
13 7 1 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
14 5 9 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
15 7 2 2polssN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
16 5 14 15 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
17 df-pss ⊢ ( ( 𝑋 + 𝑌 ) ⊊ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ↔ ( ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ( 𝑋 + 𝑌 ) ≠ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) )
18 pssnel ⊢ ( ( 𝑋 + 𝑌 ) ⊊ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) → ∃ 𝑝 ( 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
19 17 18 sylbir ⊢ ( ( ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ( 𝑋 + 𝑌 ) ≠ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) → ∃ 𝑝 ( 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
20 df-rex ⊢ ( ∃ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ↔ ∃ 𝑝 ( 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) )
21 19 20 sylibr ⊢ ( ( ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ( 𝑋 + 𝑌 ) ≠ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) → ∃ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) )
22 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
23 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
24 eqid ⊢ ( 𝑋 + { 𝑝 } ) = ( 𝑋 + { 𝑝 } )
25 eqid ⊢ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
26 22 23 7 1 2 3 24 25 osumcllem9N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + { 𝑝 } ) = 𝑋 )
27 simp11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝐾 ∈ HL )
28 simp12 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ∈ 𝐶 )
29 27 28 8 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
30 simp13 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑌 ∈ 𝐶 )
31 27 30 11 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
32 14 3adantr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
33 32 3adant3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) )
34 7 2 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
35 27 33 34 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
36 7 2 polssatN ⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ ( Atoms ‘ 𝐾 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ⊆ ( Atoms ‘ 𝐾 ) )
37 27 35 36 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ⊆ ( Atoms ‘ 𝐾 ) )
38 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
39 37 38 sseldd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
40 simp3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) )
41 22 23 7 1 2 3 24 25 osumcllem10N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + { 𝑝 } ) ≠ 𝑋 )
42 27 29 31 39 40 41 syl311anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 + { 𝑝 } ) ≠ 𝑋 )
43 26 42 pm2.21ddne ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) ∧ ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) )
44 43 3exp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → ( ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) → ( ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) ) )
45 44 3expd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) → ( 𝑋 ≠ ∅ → ( 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) → ( ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) ) ) ) )
46 45 imp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) → ( ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) ) )
47 46 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( ∃ 𝑝 ∈ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ¬ 𝑝 ∈ ( 𝑋 + 𝑌 ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
48 21 47 syl5 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( ( ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∧ ( 𝑋 + 𝑌 ) ≠ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
49 16 48 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( ( 𝑋 + 𝑌 ) ≠ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) → ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) ) )
50 49 necon1bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( ¬ ( 𝑋 = 𝑋 ∧ 𝑋 ≠ 𝑋 ) → ( 𝑋 + 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ) )
51 4 50 mpi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ ( 𝑋 ⊆ ( ⊥ ‘ 𝑌 ) ∧ 𝑋 ≠ ∅ ) ) → ( 𝑋 + 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )