Metamath Proof Explorer

Theorem iscrngo2

Description: The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Hypotheses iscring2.1 ⊢ G = 1 st ⁡ R
iscring2.2 ⊢ H = 2 nd ⁡ R
iscring2.3 ⊢ X = ran ⁡ G
Assertion iscrngo2 ⊢ R ∈ CRingOps ↔ R ∈ RingOps ∧ ∀ x ∈ X ∀ y ∈ X x H y = y H x

Proof

Step Hyp Ref Expression
1 iscring2.1 ⊢ G = 1 st ⁡ R
2 iscring2.2 ⊢ H = 2 nd ⁡ R
3 iscring2.3 ⊢ X = ran ⁡ G
4 iscrngo ⊢ R ∈ CRingOps ↔ R ∈ RingOps ∧ R ∈ Com2
5 relrngo ⊢ Rel ⁡ RingOps
6 1st2nd ⊢ Rel ⁡ RingOps ∧ R ∈ RingOps → R = 1 st ⁡ R 2 nd ⁡ R
7 5 6 mpan ⊢ R ∈ RingOps → R = 1 st ⁡ R 2 nd ⁡ R
8 eleq1 ⊢ R = 1 st ⁡ R 2 nd ⁡ R → R ∈ Com2 ↔ 1 st ⁡ R 2 nd ⁡ R ∈ Com2
9 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
10 3 9 eqtri ⊢ X = ran ⁡ 1 st ⁡ R
11 10 raleqi ⊢ ∀ x ∈ X ∀ y ∈ ran ⁡ 1 st ⁡ R x 2 nd ⁡ R y = y 2 nd ⁡ R x ↔ ∀ x ∈ ran ⁡ 1 st ⁡ R ∀ y ∈ ran ⁡ 1 st ⁡ R x 2 nd ⁡ R y = y 2 nd ⁡ R x
12 2 oveqi ⊢ x H y = x 2 nd ⁡ R y
13 2 oveqi ⊢ y H x = y 2 nd ⁡ R x
14 12 13 eqeq12i ⊢ x H y = y H x ↔ x 2 nd ⁡ R y = y 2 nd ⁡ R x
15 10 14 raleqbii ⊢ ∀ y ∈ X x H y = y H x ↔ ∀ y ∈ ran ⁡ 1 st ⁡ R x 2 nd ⁡ R y = y 2 nd ⁡ R x
16 15 ralbii ⊢ ∀ x ∈ X ∀ y ∈ X x H y = y H x ↔ ∀ x ∈ X ∀ y ∈ ran ⁡ 1 st ⁡ R x 2 nd ⁡ R y = y 2 nd ⁡ R x
17 fvex ⊢ 1 st ⁡ R ∈ V
18 fvex ⊢ 2 nd ⁡ R ∈ V
19 iscom2 ⊢ 1 st ⁡ R ∈ V ∧ 2 nd ⁡ R ∈ V → 1 st ⁡ R 2 nd ⁡ R ∈ Com2 ↔ ∀ x ∈ ran ⁡ 1 st ⁡ R ∀ y ∈ ran ⁡ 1 st ⁡ R x 2 nd ⁡ R y = y 2 nd ⁡ R x
20 17 18 19 mp2an ⊢ 1 st ⁡ R 2 nd ⁡ R ∈ Com2 ↔ ∀ x ∈ ran ⁡ 1 st ⁡ R ∀ y ∈ ran ⁡ 1 st ⁡ R x 2 nd ⁡ R y = y 2 nd ⁡ R x
21 11 16 20 3bitr4ri ⊢ 1 st ⁡ R 2 nd ⁡ R ∈ Com2 ↔ ∀ x ∈ X ∀ y ∈ X x H y = y H x
22 8 21 bitrdi ⊢ R = 1 st ⁡ R 2 nd ⁡ R → R ∈ Com2 ↔ ∀ x ∈ X ∀ y ∈ X x H y = y H x
23 7 22 syl ⊢ R ∈ RingOps → R ∈ Com2 ↔ ∀ x ∈ X ∀ y ∈ X x H y = y H x
24 23 pm5.32i ⊢ R ∈ RingOps ∧ R ∈ Com2 ↔ R ∈ RingOps ∧ ∀ x ∈ X ∀ y ∈ X x H y = y H x
25 4 24 bitri ⊢ R ∈ CRingOps ↔ R ∈ RingOps ∧ ∀ x ∈ X ∀ y ∈ X x H y = y H x