Metamath Proof Explorer

Theorem elpaddri

Description: Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012)

Ref Expression
Hypotheses paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion elpaddri ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ∈ ( 𝑋 + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simp3l ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ∈ 𝐴 )
6 simp2l ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑄 ∈ 𝑋 )
7 simp2r ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝑌 )
8 simp3r ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) )
9 oveq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) )
10 9 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑟 ) ) )
11 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑅 ) )
12 11 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑆 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
13 10 12 rspc2ev ⊢ ( ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) )
14 6 7 8 13 syl3anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) )
15 ne0i ⊢ ( 𝑄 ∈ 𝑋 → 𝑋 ≠ ∅ )
16 ne0i ⊢ ( 𝑅 ∈ 𝑌 → 𝑌 ≠ ∅ )
17 15 16 anim12i ⊢ ( ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) → ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) )
18 17 anim2i ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ) → ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) )
19 18 3adant3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) )
20 1 2 3 4 elpaddn0 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
21 19 20 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
22 5 14 21 mpbir2and ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑆 ∈ ( 𝑋 + 𝑌 ) )