Description: Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | paddssw.a | |
|
paddssw.p | |
||
Assertion | paddssw2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | paddssw.a | |
|
2 | paddssw.p | |
|
3 | 1 2 | sspadd1 | |
4 | 3 | 3adant3r3 | |
5 | sstr | |
|
6 | 4 5 | sylan | |
7 | 6 | ex | |
8 | simpl | |
|
9 | simpr2 | |
|
10 | simpr1 | |
|
11 | 1 2 | sspadd2 | |
12 | 8 9 10 11 | syl3anc | |
13 | sstr | |
|
14 | 12 13 | sylan | |
15 | 14 | ex | |
16 | 7 15 | jcad | |