Theorem paddval0

Description: Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012)

	Ref	Expression
Hypotheses	padd0.a	|- A = ( Atoms ` K )
	padd0.p	|- .+ = ( +P ` K )
Assertion	paddval0	|- ( ( ( K e. B /\ X C_ A /\ Y C_ A ) /\ -. ( X =/= (/) /\ Y =/= (/) ) ) -> ( X .+ Y ) = ( X u. Y ) )

Proof

Step	Hyp	Ref	Expression
1		padd0.a	|- A = ( Atoms ` K )
2		padd0.p	|- .+ = ( +P ` K )
3	1 2	elpadd0	|- ( ( ( K e. B /\ X C_ A /\ Y C_ A ) /\ -. ( X =/= (/) /\ Y =/= (/) ) ) -> ( q e. ( X .+ Y ) <-> ( q e. X \/ q e. Y ) ) )
4		elun	|- ( q e. ( X u. Y ) <-> ( q e. X \/ q e. Y ) )
5	3 4	bitr4di	|- ( ( ( K e. B /\ X C_ A /\ Y C_ A ) /\ -. ( X =/= (/) /\ Y =/= (/) ) ) -> ( q e. ( X .+ Y ) <-> q e. ( X u. Y ) ) )
6	5	eqrdv	|- ( ( ( K e. B /\ X C_ A /\ Y C_ A ) /\ -. ( X =/= (/) /\ Y =/= (/) ) ) -> ( X .+ Y ) = ( X u. Y ) )