This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )