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 ) |
| 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 ) |