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

Metamath Proof Explorer

Theorem elpaddatriN

Description: Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ = ( le ‘ 𝐾 )
2 paddfval.j ⊢ ∨ = ( join ‘ 𝐾 )
3 paddfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 paddfval.p ⊢ + = ( +𝑃 ‘ 𝐾 )
5 simpl1 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝐾 ∈ Lat )
6 simpl2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑋 ⊆ 𝐴 )
7 simpl3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐴 )
8 7 snssd ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → { 𝑄 } ⊆ 𝐴 )
9 simpr1 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑅 ∈ 𝑋 )
10 snidg ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ { 𝑄 } )
11 7 10 syl ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑄 ∈ { 𝑄 } )
12 simpr2 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑆 ∈ 𝐴 )
13 simpr3 ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) )
14 1 2 3 4 elpaddri ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ { 𝑄 } ⊆ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑄 ∈ { 𝑄 } ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( 𝑋 + { 𝑄 } ) )
15 5 6 8 9 11 12 13 14 syl322anc ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( 𝑋 + { 𝑄 } ) )