Step |
Hyp |
Ref |
Expression |
1 |
|
0r |
|- 0R e. R. |
2 |
|
addcnsr |
|- ( ( ( A e. R. /\ 0R e. R. ) /\ ( B e. R. /\ 0R e. R. ) ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , ( 0R +R 0R ) >. ) |
3 |
2
|
an4s |
|- ( ( ( A e. R. /\ B e. R. ) /\ ( 0R e. R. /\ 0R e. R. ) ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , ( 0R +R 0R ) >. ) |
4 |
1 1 3
|
mpanr12 |
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , ( 0R +R 0R ) >. ) |
5 |
|
0idsr |
|- ( 0R e. R. -> ( 0R +R 0R ) = 0R ) |
6 |
1 5
|
ax-mp |
|- ( 0R +R 0R ) = 0R |
7 |
6
|
opeq2i |
|- <. ( A +R B ) , ( 0R +R 0R ) >. = <. ( A +R B ) , 0R >. |
8 |
4 7
|
eqtrdi |
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , 0R >. ) |