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	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ E + [ ⟨ 𝐶 , 𝐷 ⟩ ] ◡ E ) = [ ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ ] ◡ E )

Proof

Step	Hyp	Ref	Expression
1		addcnsr	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ + ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ )
2		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
3	2	ecid	⊢ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ E = ⟨ 𝐴 , 𝐵 ⟩
4		opex	⊢ ⟨ 𝐶 , 𝐷 ⟩ ∈ V
5	4	ecid	⊢ [ ⟨ 𝐶 , 𝐷 ⟩ ] ◡ E = ⟨ 𝐶 , 𝐷 ⟩
6	3 5	oveq12i	⊢ ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ E + [ ⟨ 𝐶 , 𝐷 ⟩ ] ◡ E ) = ( ⟨ 𝐴 , 𝐵 ⟩ + ⟨ 𝐶 , 𝐷 ⟩ )
7		opex	⊢ ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ ∈ V
8	7	ecid	⊢ [ ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ ] ◡ E = ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩
9	1 6 8	3eqtr4g	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ E + [ ⟨ 𝐶 , 𝐷 ⟩ ] ◡ E ) = [ ⟨ ( 𝐴 +R 𝐶 ) , ( 𝐵 +R 𝐷 ) ⟩ ] ◡ E )