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

Proof

Step	Hyp	Ref	Expression
1		mulcnsr	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ · ⟨ 𝐶 , 𝐷 ⟩ ) = ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·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 ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ ∈ V
8	7	ecid	⊢ [ ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ ] ◡ E = ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩
9	1 6 8	3eqtr4g	⊢ ( ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) ∧ ( 𝐶 ∈ R ∧ 𝐷 ∈ R ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ E · [ ⟨ 𝐶 , 𝐷 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝐴 ·R 𝐶 ) +R ( -1R ·R ( 𝐵 ·R 𝐷 ) ) ) , ( ( 𝐵 ·R 𝐶 ) +R ( 𝐴 ·R 𝐷 ) ) ⟩ ] ◡ E )