Theorem paddvaln0N

Description: Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	paddfval.l	|- .<_ = ( le ` K )
	paddfval.j	|- .\/ = ( join ` K )
	paddfval.a	|- A = ( Atoms ` K )
	paddfval.p	|- .+ = ( +P ` K )
Assertion	paddvaln0N	|- ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( X .+ Y ) = { p e. A | E. q e. X E. r e. Y p .<_ ( 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	elpaddn0	|- ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( s e. ( X .+ Y ) <-> ( s e. A /\ E. q e. X E. r e. Y s .<_ ( q .\/ r ) ) ) )
6		breq1	|- ( p = s -> ( p .<_ ( q .\/ r ) <-> s .<_ ( q .\/ r ) ) )
7	6	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 ) ) )
8	7	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 ) ) )
9	5 8	bitr4di	|- ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( s e. ( X .+ Y ) <-> s e. { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } ) )
10	9	eqrdv	|- ( ( ( K e. Lat /\ X C_ A /\ Y C_ A ) /\ ( X =/= (/) /\ Y =/= (/) ) ) -> ( X .+ Y ) = { p e. A | E. q e. X E. r e. Y p .<_ ( q .\/ r ) } )