Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  paddclN Structured version   Unicode version

 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.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp1 958 . . 3
2 eqid 2443 . . . . 5
3 paddidm.s . . . . 5
42, 3psubssat 30725 . . . 4
62, 3psubssat 30725 . . . 4
8 paddidm.p . . . 4
92, 8paddssat 30785 . . 3
101, 5, 7, 9syl3anc 1185 . 2
11 olc 375 . . . . 5
12 eqid 2443 . . . . . . . 8
13 eqid 2443 . . . . . . . 8
1412, 13, 2, 8elpadd 30770 . . . . . . 7
151, 10, 10, 14syl3anc 1185 . . . . . 6
162, 8padd4N 30811 . . . . . . . . 9
171, 5, 7, 5, 7, 16syl122anc 1194 . . . . . . . 8
183, 8paddidm 30812 . . . . . . . . . 10
19183adant3 978 . . . . . . . . 9
203, 8paddidm 30812 . . . . . . . . . 10
21203adant2 977 . . . . . . . . 9
2219, 21oveq12d 6135 . . . . . . . 8
2317, 22eqtrd 2475 . . . . . . 7
2423eleq2d 2510 . . . . . 6
2515, 24bitr3d 248 . . . . 5
2611, 25syl5ib 212 . . . 4
2726exp3a 427 . . 3
2827ralrimiv 2795 . 2
2912, 13, 2, 3ispsubsp2 30717 . . 3