Theorem padd02

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

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

Proof

Step	Hyp	Ref	Expression
1		padd0.a	|- A = ( Atoms ` K )
2		padd0.p	|- .+ = ( +P ` K )
3		simpl	|- ( ( K e. B /\ X C_ A ) -> K e. B )
4		0ss	|- (/) C_ A
5	4	a1i	|- ( ( K e. B /\ X C_ A ) -> (/) C_ A )
6		simpr	|- ( ( K e. B /\ X C_ A ) -> X C_ A )
7	3 5 6	3jca	|- ( ( K e. B /\ X C_ A ) -> ( K e. B /\ (/) C_ A /\ X C_ A ) )
8		neirr	|- -. (/) =/= (/)
9	8	intnanr	|- -. ( (/) =/= (/) /\ X =/= (/) )
10	1 2	paddval0	|- ( ( ( K e. B /\ (/) C_ A /\ X C_ A ) /\ -. ( (/) =/= (/) /\ X =/= (/) ) ) -> ( (/) .+ X ) = ( (/) u. X ) )
11	7 9 10	sylancl	|- ( ( K e. B /\ X C_ A ) -> ( (/) .+ X ) = ( (/) u. X ) )
12		uncom	|- ( (/) u. X ) = ( X u. (/) )
13		un0	|- ( X u. (/) ) = X
14	12 13	eqtri	|- ( (/) u. X ) = X
15	11 14	eqtrdi	|- ( ( K e. B /\ X C_ A ) -> ( (/) .+ X ) = X )