Description: The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of MaedaMaeda p. 68. (Contributed by NM, 14-Jan-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | paddidm.s | |
|
paddidm.p | |
||
Assertion | paddclN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | paddidm.s | |
|
2 | paddidm.p | |
|
3 | simp1 | |
|
4 | eqid | |
|
5 | 4 1 | psubssat | |
6 | 5 | 3adant3 | |
7 | 4 1 | psubssat | |
8 | 7 | 3adant2 | |
9 | 4 2 | paddssat | |
10 | 3 6 8 9 | syl3anc | |
11 | olc | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | 12 13 4 2 | elpadd | |
15 | 3 10 10 14 | syl3anc | |
16 | 4 2 | padd4N | |
17 | 3 6 8 6 8 16 | syl122anc | |
18 | 1 2 | paddidm | |
19 | 18 | 3adant3 | |
20 | 1 2 | paddidm | |
21 | 20 | 3adant2 | |
22 | 19 21 | oveq12d | |
23 | 17 22 | eqtrd | |
24 | 23 | eleq2d | |
25 | 15 24 | bitr3d | |
26 | 11 25 | syl5ib | |
27 | 26 | expd | |
28 | 27 | ralrimiv | |
29 | 12 13 4 1 | ispsubsp2 | |
30 | 29 | 3ad2ant1 | |
31 | 10 28 30 | mpbir2and | |