Metamath Proof Explorer

Theorem elpadd0

Description: Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 padd0.a 
 |-  A = ( Atoms ` K )
2 padd0.p 
 |-  .+ = ( +P ` K )
3 neanior 
 |-  ( ( X =/= (/) /\ Y =/= (/) ) <-> -. ( X = (/) \/ Y = (/) ) )
4 3 bicomi 
 |-  ( -. ( X = (/) \/ Y = (/) ) <-> ( X =/= (/) /\ Y =/= (/) ) )
5 4 con1bii 
 |-  ( -. ( X =/= (/) /\ Y =/= (/) ) <-> ( X = (/) \/ Y = (/) ) )
6 eqid 
 |-  ( le ` K ) = ( le ` K )
7 eqid 
 |-  ( join ` K ) = ( join ` K )
8 6 7 1 2 elpadd 
 |-  ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( S e. ( X .+ Y ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) ) ) )
9 rex0 
 |-  -. E. q e. (/) E. r e. Y S ( le ` K ) ( q ( join ` K ) r )
10 rexeq 
 |-  ( X = (/) -> ( E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) <-> E. q e. (/) E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) )
11 9 10 mtbiri 
 |-  ( X = (/) -> -. E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) )
12 rex0 
 |-  -. E. r e. (/) S ( le ` K ) ( q ( join ` K ) r )
13 12 a1i 
 |-  ( q e. X -> -. E. r e. (/) S ( le ` K ) ( q ( join ` K ) r ) )
14 13 nrex 
 |-  -. E. q e. X E. r e. (/) S ( le ` K ) ( q ( join ` K ) r )
15 rexeq 
 |-  ( Y = (/) -> ( E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) <-> E. r e. (/) S ( le ` K ) ( q ( join ` K ) r ) ) )
16 15 rexbidv 
 |-  ( Y = (/) -> ( E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) <-> E. q e. X E. r e. (/) S ( le ` K ) ( q ( join ` K ) r ) ) )
17 14 16 mtbiri 
 |-  ( Y = (/) -> -. E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) )
18 11 17 jaoi 
 |-  ( ( X = (/) \/ Y = (/) ) -> -. E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) )
19 18 intnand 
 |-  ( ( X = (/) \/ Y = (/) ) -> -. ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) )
20 biorf 
 |-  ( -. ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) -> ( ( S e. X \/ S e. Y ) <-> ( ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) \/ ( S e. X \/ S e. Y ) ) ) )
21 19 20 syl 
 |-  ( ( X = (/) \/ Y = (/) ) -> ( ( S e. X \/ S e. Y ) <-> ( ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) \/ ( S e. X \/ S e. Y ) ) ) )
22 orcom 
 |-  ( ( ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) \/ ( S e. X \/ S e. Y ) ) <-> ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) ) )
23 21 22 bitr2di 
 |-  ( ( X = (/) \/ Y = (/) ) -> ( ( ( S e. X \/ S e. Y ) \/ ( S e. A /\ E. q e. X E. r e. Y S ( le ` K ) ( q ( join ` K ) r ) ) ) <-> ( S e. X \/ S e. Y ) ) )
24 8 23 sylan9bb 
 |-  ( ( ( K e. B /\ X C_ A /\ Y C_ A ) /\ ( X = (/) \/ Y = (/) ) ) -> ( S e. ( X .+ Y ) <-> ( S e. X \/ S e. Y ) ) )
25 5 24 sylan2b 
 |-  ( ( ( K e. B /\ X C_ A /\ Y C_ A ) /\ -. ( X =/= (/) /\ Y =/= (/) ) ) -> ( S e. ( X .+ Y ) <-> ( S e. X \/ S e. Y ) ) )