Description: Subset law for projective subspace sum. ( unss1 analog.) (Contributed by NM, 7-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | padd0.a | |
|
padd0.p | |
||
Assertion | paddss1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | padd0.a | |
|
2 | padd0.p | |
|
3 | ssel | |
|
4 | 3 | orim1d | |
5 | ssrexv | |
|
6 | 5 | anim2d | |
7 | 4 6 | orim12d | |
8 | 7 | adantl | |
9 | simpl1 | |
|
10 | sstr | |
|
11 | 10 | 3ad2antr2 | |
12 | 11 | ancoms | |
13 | simpl3 | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 14 15 1 2 | elpadd | |
17 | 9 12 13 16 | syl3anc | |
18 | 14 15 1 2 | elpadd | |
19 | 18 | adantr | |
20 | 8 17 19 | 3imtr4d | |
21 | 20 | ssrdv | |
22 | 21 | ex | |