Metamath Proof Explorer

Theorem crngocom

Description: The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Hypotheses crngocom.1 ⊢ G = 1 st ⁡ R
crngocom.2 ⊢ H = 2 nd ⁡ R
crngocom.3 ⊢ X = ran ⁡ G
Assertion crngocom ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X → A H B = B H A

Proof

Step Hyp Ref Expression
1 crngocom.1 ⊢ G = 1 st ⁡ R
2 crngocom.2 ⊢ H = 2 nd ⁡ R
3 crngocom.3 ⊢ X = ran ⁡ G
4 1 2 3 iscrngo2 ⊢ R ∈ CRingOps ↔ R ∈ RingOps ∧ ∀ x ∈ X ∀ y ∈ X x H y = y H x
5 4 simprbi ⊢ R ∈ CRingOps → ∀ x ∈ X ∀ y ∈ X x H y = y H x
6 oveq1 ⊢ x = A → x H y = A H y
7 oveq2 ⊢ x = A → y H x = y H A
8 6 7 eqeq12d ⊢ x = A → x H y = y H x ↔ A H y = y H A
9 oveq2 ⊢ y = B → A H y = A H B
10 oveq1 ⊢ y = B → y H A = B H A
11 9 10 eqeq12d ⊢ y = B → A H y = y H A ↔ A H B = B H A
12 8 11 rspc2v ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X ∀ y ∈ X x H y = y H x → A H B = B H A
13 5 12 mpan9 ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X → A H B = B H A
14 13 3impb ⊢ R ∈ CRingOps ∧ A ∈ X ∧ B ∈ X → A H B = B H A