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 ( ( ( 𝐴 ∈ 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 )