Theorem elpadd2at

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

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

Proof

Step	Hyp	Ref	Expression
1		paddfval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		paddfval.j	⊢ ∨ = ( join ‘ 𝐾 )
3		paddfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		paddfval.p	⊢ + = ( +𝑃 ‘ 𝐾 )
5		simp1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → 𝐾 ∈ Lat )
6		simp2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
7	6	snssd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → { 𝑄 } ⊆ 𝐴 )
8		simp3	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → 𝑅 ∈ 𝐴 )
9		snnzg	⊢ ( 𝑄 ∈ 𝐴 → { 𝑄 } ≠ ∅ )
10	9	3ad2ant2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → { 𝑄 } ≠ ∅ )
11	1 2 3 4	elpaddat	⊢ ( ( ( 𝐾 ∈ Lat ∧ { 𝑄 } ⊆ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ { 𝑄 } ≠ ∅ ) → ( 𝑆 ∈ ( { 𝑄 } + { 𝑅 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑟 ∨ 𝑅 ) ) ) )
12	5 7 8 10 11	syl31anc	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑆 ∈ ( { 𝑄 } + { 𝑅 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑟 ∨ 𝑅 ) ) ) )
13		oveq1	⊢ ( 𝑟 = 𝑄 → ( 𝑟 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
14	13	breq2d	⊢ ( 𝑟 = 𝑄 → ( 𝑆 ≤ ( 𝑟 ∨ 𝑅 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
15	14	rexsng	⊢ ( 𝑄 ∈ 𝐴 → ( ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑟 ∨ 𝑅 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
16	15	3ad2ant2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑟 ∨ 𝑅 ) ↔ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) )
17	16	anbi2d	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑟 ∨ 𝑅 ) ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
18	12 17	bitrd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑆 ∈ ( { 𝑄 } + { 𝑅 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )