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

Metamath Proof Explorer

Theorem elpadd0

Description: Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011)

Ref Expression
Hypotheses padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion elpadd0 ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 padd0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 neanior ⊢ ( ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ↔ ¬ ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) )
4 3 bicomi ⊢ ( ¬ ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) ↔ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) )
5 4 con1bii ⊢ ( ¬ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ↔ ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
8 6 7 1 2 elpadd ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ) )
9 rex0 ⊢ ¬ ∃ 𝑞 ∈ ∅ ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 )
10 rexeq ⊢ ( 𝑋 = ∅ → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ↔ ∃ 𝑞 ∈ ∅ ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
11 9 10 mtbiri ⊢ ( 𝑋 = ∅ → ¬ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
12 rex0 ⊢ ¬ ∃ 𝑟 ∈ ∅ 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 )
13 12 a1i ⊢ ( 𝑞 ∈ 𝑋 → ¬ ∃ 𝑟 ∈ ∅ 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
14 13 nrex ⊢ ¬ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ ∅ 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 )
15 rexeq ⊢ ( 𝑌 = ∅ → ( ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ↔ ∃ 𝑟 ∈ ∅ 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
16 15 rexbidv ⊢ ( 𝑌 = ∅ → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ ∅ 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
17 14 16 mtbiri ⊢ ( 𝑌 = ∅ → ¬ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
18 11 17 jaoi ⊢ ( ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) → ¬ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) )
19 18 intnand ⊢ ( ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) → ¬ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) )
20 biorf ⊢ ( ¬ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) → ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ↔ ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ∨ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) ) )
21 19 20 syl ⊢ ( ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) → ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ↔ ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ∨ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) ) )
22 orcom ⊢ ( ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ∨ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) )
23 21 22 bitr2di ⊢ ( ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) → ( ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ) ) ↔ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) )
24 8 23 sylan9bb ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 = ∅ ∨ 𝑌 = ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) )
25 5 24 sylan2b ⊢ ( ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ¬ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ) )