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 ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 ∧ D ∈ 𝑹 → A B E -1 ⁢ C D E -1 = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D E -1

Proof

Step Hyp Ref Expression
1 mulcnsr ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 ∧ D ∈ 𝑹 → A B ⁢ C D = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D
2 opex ⊢ A B ∈ V
3 2 ecid ⊢ A B E -1 = A B
4 opex ⊢ C D ∈ V
5 4 ecid ⊢ C D E -1 = C D
6 3 5 oveq12i ⊢ A B E -1 ⁢ C D E -1 = A B ⁢ C D
7 opex ⊢ A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D ∈ V
8 7 ecid ⊢ A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D E -1 = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D
9 1 6 8 3eqtr4g ⊢ A ∈ 𝑹 ∧ B ∈ 𝑹 ∧ C ∈ 𝑹 ∧ D ∈ 𝑹 → A B E -1 ⁢ C D E -1 = A ⋅ 𝑹 C + 𝑹 -1 𝑹 ⋅ 𝑹 B ⋅ 𝑹 D B ⋅ 𝑹 C + 𝑹 A ⋅ 𝑹 D E -1