Theorem elpadd

Description: Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011)

	Ref	Expression
Hypotheses	paddfval.l	⊢ ≤ = ( le ‘ 𝐾 )
	paddfval.j	⊢ ∨ = ( join ‘ 𝐾 )
	paddfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	paddfval.p	⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion	elpadd	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ) )

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	paddval	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
6	5	eleq2d	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ 𝑆 ∈ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
7		elun	⊢ ( 𝑆 ∈ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ( 𝑆 ∈ ( 𝑋 ∪ 𝑌 ) ∨ 𝑆 ∈ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
8		elun	⊢ ( 𝑆 ∈ ( 𝑋 ∪ 𝑌 ) ↔ ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) )
9		breq1	⊢ ( 𝑝 = 𝑆 → ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
10	9	2rexbidv	⊢ ( 𝑝 = 𝑆 → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
11	10	elrab	⊢ ( 𝑆 ∈ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ↔ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) )
12	8 11	orbi12i	⊢ ( ( 𝑆 ∈ ( 𝑋 ∪ 𝑌 ) ∨ 𝑆 ∈ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
13	7 12	bitri	⊢ ( 𝑆 ∈ ( ( 𝑋 ∪ 𝑌 ) ∪ { 𝑝 ∈ 𝐴 ∣ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) )
14	6 13	bitrdi	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑆 ∈ ( 𝑋 + 𝑌 ) ↔ ( ( 𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌 ) ∨ ( 𝑆 ∈ 𝐴 ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑌 𝑆 ≤ ( 𝑞 ∨ 𝑟 ) ) ) ) )