Theorem padd01

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	padd01	|- ( ( 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		simpr	|- ( ( K e. B /\ X C_ A ) -> X C_ A )
5		0ss	|- (/) C_ A
6	5	a1i	|- ( ( K e. B /\ X C_ A ) -> (/) C_ A )
7	3 4 6	3jca	|- ( ( K e. B /\ X C_ A ) -> ( K e. B /\ X C_ A /\ (/) C_ A ) )
8		neirr	|- -. (/) =/= (/)
9	8	intnan	|- -. ( X =/= (/) /\ (/) =/= (/) )
10	1 2	paddval0	|- ( ( ( K e. B /\ X C_ A /\ (/) C_ A ) /\ -. ( X =/= (/) /\ (/) =/= (/) ) ) -> ( X .+ (/) ) = ( X u. (/) ) )
11	7 9 10	sylancl	|- ( ( K e. B /\ X C_ A ) -> ( X .+ (/) ) = ( X u. (/) ) )
12		un0	|- ( X u. (/) ) = X
13	11 12	eqtrdi	|- ( ( K e. B /\ X C_ A ) -> ( X .+ (/) ) = X )