| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mulcnsrec | Structured version Visualization version GIF version | ||
| Description: Technical trick to permit
re-use of some equivalence class lemmas for
operation laws. The trick involves ecid 8718,
which shows that the coset of
the converse membership relation (which is not an equivalence relation)
leaves a set unchanged. See also dfcnqs 11054.
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 10756. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| mulcnsrec | ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mulcnsr 11048 | . 2 ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) = 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉) | |
| 2 | opex 5409 | . . . 4 ⊢ 〈𝐴, 𝐵〉 ∈ V | |
| 3 | 2 | ecid 8718 | . . 3 ⊢ [〈𝐴, 𝐵〉]◡ E = 〈𝐴, 𝐵〉 |
| 4 | opex 5409 | . . . 4 ⊢ 〈𝐶, 𝐷〉 ∈ V | |
| 5 | 4 | ecid 8718 | . . 3 ⊢ [〈𝐶, 𝐷〉]◡ E = 〈𝐶, 𝐷〉 |
| 6 | 3, 5 | oveq12i 7370 | . 2 ⊢ ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = (〈𝐴, 𝐵〉 · 〈𝐶, 𝐷〉) |
| 7 | opex 5409 | . . 3 ⊢ 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉 ∈ V | |
| 8 | 7 | ecid 8718 | . 2 ⊢ [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E = 〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉 |
| 9 | 1, 6, 8 | 3eqtr4g 2797 | 1 ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (𝐶 ∈ R ∧ 𝐷 ∈ R)) → ([〈𝐴, 𝐵〉]◡ E · [〈𝐶, 𝐷〉]◡ E ) = [〈((𝐴 ·R 𝐶) +R (-1R ·R (𝐵 ·R 𝐷))), ((𝐵 ·R 𝐶) +R (𝐴 ·R 𝐷))〉]◡ E ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 〈cop 4574 E cep 5521 ◡ccnv 5621 (class class class)co 7358 [cec 8632 Rcnr 10777 -1Rcm1r 10780 +R cplr 10781 ·R cmr 10782 · cmul 11032 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-pr 5368 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-id 5517 df-eprel 5522 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fv 6498 df-ov 7361 df-oprab 7362 df-ec 8636 df-c 11033 df-mul 11039 |
| This theorem is referenced by: axmulcom 11067 axmulass 11069 axdistr 11070 |
| Copyright terms: Public domain | W3C validator |