This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcnsrec

Description: Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs and mulcnsrec . (Contributed by NM, 13-Aug-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	addcnsrec	$⊢ ((A \in 𝑹 \land B \in 𝑹) \land (C \in 𝑹 \land D \in 𝑹)) \to [⟨A, B⟩] E^{-1} + [⟨C, D⟩] E^{-1} = [⟨A +_{𝑹} C, B +_{𝑹} D⟩] E^{-1}$

Proof

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