This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcnsrec

Description: Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs and mulcnsrec . (Contributed by NM, 13-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion addcnsrec 
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E + [ <. C , D >. ] `' _E ) = [ <. ( A +R C ) , ( B +R D ) >. ] `' _E )

Proof

Step Hyp Ref Expression
1 addcnsr 
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. + <. C , D >. ) = <. ( A +R C ) , ( B +R D ) >. )
2 opex 
 |-  <. A , B >. e. _V
3 2 ecid 
 |-  [ <. A , B >. ] `' _E = <. A , B >.
4 opex 
 |-  <. C , D >. e. _V
5 4 ecid 
 |-  [ <. C , D >. ] `' _E = <. C , D >.
6 3 5 oveq12i 
 |-  ( [ <. A , B >. ] `' _E + [ <. C , D >. ] `' _E ) = ( <. A , B >. + <. C , D >. )
7 opex 
 |-  <. ( A +R C ) , ( B +R D ) >. e. _V
8 7 ecid 
 |-  [ <. ( A +R C ) , ( B +R D ) >. ] `' _E = <. ( A +R C ) , ( B +R D ) >.
9 1 6 8 3eqtr4g 
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E + [ <. C , D >. ] `' _E ) = [ <. ( A +R C ) , ( B +R D ) >. ] `' _E )