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 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑅 ∨ 𝑄 ) ) ) → 𝑆 ∈ ( 𝑋 + { 𝑄 } ) )