Theorem elpadd

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

	Ref	Expression
Hypotheses	paddfval.l	|- .<_ = ( le ` K )
	paddfval.j	|- .\/ = ( join ` K )
	paddfval.a	|- A = ( Atoms ` K )
	paddfval.p	|- .+ = ( +P ` K )
Assertion	elpadd	|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( S e. ( X .+ Y ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		paddfval.l	|- .<_ = ( le ` K )
2		paddfval.j	|- .\/ = ( join ` K )
3		paddfval.a	|- A = ( Atoms ` K )
4		paddfval.p	|- .+ = ( +P ` K )
5	1 2 3 4	paddval	|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
6	5	eleq2d	|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( S e. ( X .+ Y ) <-> S e. ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) ) )
7		elun	|- ( S e. ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) <-> ( S e. ( X u. Y ) \/ S e. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
8		elun	|- ( S e. ( X u. Y ) <-> ( S e. X \/ S e. Y ) )
9		breq1	|- ( p = S -> ( p .<_ ( q .\/ r ) <-> S .<_ ( q .\/ r ) ) )
10	9	2rexbidv	|- ( p = S -> ( E. q e. X E. r e. Y p .<_ ( q .\/ r ) <-> E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
11	10	elrab	|- ( S e. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } <-> ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) )
12	8 11	orbi12i	|- ( ( S e. ( X u. Y ) \/ S e. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
13	7 12	bitri	|- ( S e. ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) )
14	6 13	bitrdi	|- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( S e. ( X .+ Y ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S .<_ ( q .\/ r ) ) ) ) )