Theorem elpaddat

Description: Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012)

	Ref	Expression
Hypotheses	paddfval.l	⊢ ≤ = ( le ‘ 𝐾 )
	paddfval.j	⊢ ∨ = ( join ‘ 𝐾 )
	paddfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	paddfval.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	elpaddat	⊢ ( ( ( 𝐾 ∈ 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		simpr	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → 𝑋 ≠ ∅ )
10	7	snn0d	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → { 𝑄 } ≠ ∅ )
11	1 2 3 4	elpaddn0	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ { 𝑄 } ⊆ 𝐴 ) ∧ ( 𝑋 ≠ ∅ ∧ { 𝑄 } ≠ ∅ ) ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ) ) )
12	5 6 8 9 10 11	syl32anc	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ) ) )
13		oveq2	⊢ ( 𝑟 = 𝑄 → ( 𝑝 ∨ 𝑟 ) = ( 𝑝 ∨ 𝑄 ) )
14	13	breq2d	⊢ ( 𝑟 = 𝑄 → ( 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
15	14	rexsng	⊢ ( 𝑄 ∈ 𝐴 → ( ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
16	7 15	syl	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
17	16	rexbidv	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ↔ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) )
18	17	anbi2d	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 ∃ 𝑟 ∈ { 𝑄 } 𝑆 ≤ ( 𝑝 ∨ 𝑟 ) ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) ) )
19	12 18	bitrd	⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑋 ≠ ∅ ) → ( 𝑆 ∈ ( 𝑋 + { 𝑄 } ) ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑝 ∈ 𝑋 𝑆 ≤ ( 𝑝 ∨ 𝑄 ) ) ) )