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 \in 𝑹 \land B \in 𝑹) \land (C \in 𝑹 \land D \in 𝑹)) \to [⟨A, B⟩] E^{-1} [⟨C, D⟩] E^{-1} = [⟨(A \cdot_{𝑹} C) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (B \cdot_{𝑹} D)), (B \cdot_{𝑹} C) +_{𝑹} (A \cdot_{𝑹} D)⟩] E^{-1}$

Proof

Step	Hyp	Ref	Expression
1		mulcnsr	$⊢ ((A \in 𝑹 \land B \in 𝑹) \land (C \in 𝑹 \land D \in 𝑹)) \to ⟨A, B⟩ ⟨C, D⟩ = ⟨(A \cdot_{𝑹} C) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (B \cdot_{𝑹} D)), (B \cdot_{𝑹} C) +_{𝑹} (A \cdot_{𝑹} D)⟩$
2		opex	$⊢ ⟨A, B⟩ \in V$
3	2	ecid	$⊢ [⟨A, B⟩] E^{-1} = ⟨A, B⟩$
4		opex	$⊢ ⟨C, D⟩ \in 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 \cdot_{𝑹} C) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (B \cdot_{𝑹} D)), (B \cdot_{𝑹} C) +_{𝑹} (A \cdot_{𝑹} D)⟩ \in V$
8	7	ecid	$⊢ [⟨(A \cdot_{𝑹} C) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (B \cdot_{𝑹} D)), (B \cdot_{𝑹} C) +_{𝑹} (A \cdot_{𝑹} D)⟩] E^{-1} = ⟨(A \cdot_{𝑹} C) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (B \cdot_{𝑹} D)), (B \cdot_{𝑹} C) +_{𝑹} (A \cdot_{𝑹} D)⟩$
9	1 6 8	3eqtr4g	$⊢ ((A \in 𝑹 \land B \in 𝑹) \land (C \in 𝑹 \land D \in 𝑹)) \to [⟨A, B⟩] E^{-1} [⟨C, D⟩] E^{-1} = [⟨(A \cdot_{𝑹} C) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (B \cdot_{𝑹} D)), (B \cdot_{𝑹} C) +_{𝑹} (A \cdot_{𝑹} D)⟩] E^{-1}$

Metamath Proof Explorer

Theorem mulcnsrec

Proof