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