Theorem elpadd2at2

Description: Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012)

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

Proof

Step	Hyp	Ref	Expression
1		paddfval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		paddfval.j	⊢ ∨ = ( join ‘ 𝐾 )
3		paddfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		paddfval.p	⊢ + = ( +𝑃 ‘ 𝐾 )
5	1 2 3 4	elpadd2at	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑆 ∈ ( { 𝑄 } + { 𝑅 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
6	5	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ∈ ( { 𝑄 } + { 𝑅 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
7		simpr3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
8	7	biantrurd	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
9	6 8	bitr4d	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑆 ∈ ( { 𝑄 } + { 𝑅 } ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )