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

Metamath Proof Explorer

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 )