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 )