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

 Description: Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uncom 3491 . . . 4
21a1i 11 . . 3
3 simpl1 960 . . . . . . . 8
4 simpl2 961 . . . . . . . . . 10
5 simprl 733 . . . . . . . . . 10
64, 5sseldd 3349 . . . . . . . . 9
7 eqid 2436 . . . . . . . . . 10
8 padd0.a . . . . . . . . . 10
97, 8atbase 30087 . . . . . . . . 9
106, 9syl 16 . . . . . . . 8
11 simpl3 962 . . . . . . . . . 10
12 simprr 734 . . . . . . . . . 10
1311, 12sseldd 3349 . . . . . . . . 9
147, 8atbase 30087 . . . . . . . . 9
1513, 14syl 16 . . . . . . . 8
16 eqid 2436 . . . . . . . . 9
177, 16latjcom 14488 . . . . . . . 8
183, 10, 15, 17syl3anc 1184 . . . . . . 7
1918breq2d 4224 . . . . . 6
20192rexbidva 2746 . . . . 5
21 rexcom 2869 . . . . 5
2220, 21syl6bb 253 . . . 4
2322rabbidv 2948 . . 3
242, 23uneq12d 3502 . 2
25 eqid 2436 . . 3