Metamath Proof Explorer


Theorem mulcnsrec

Description: Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecid , which shows that the coset of the converse membership relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs .

Note: This is the last lemma (from which the axioms will be derived) in the construction of real and complex numbers. The construction starts at cnpi . (Contributed by NM, 13-Aug-1995) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mulcnsr
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. x. <. C , D >. ) = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .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 x. [ <. C , D >. ] `' _E ) = ( <. A , B >. x. <. C , D >. )
7 opex
 |-  <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. e. _V
8 7 ecid
 |-  [ <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. ] `' _E = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >.
9 1 6 8 3eqtr4g
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E x. [ <. C , D >. ] `' _E ) = [ <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. ] `' _E )