Metamath Proof Explorer


Theorem rngoi

Description: The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007) (Proof shortened by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ringi.1 G = 1 st R
ringi.2 H = 2 nd R
ringi.3 X = ran G
Assertion rngoi R RingOps G AbelOp H : X × X X x X y X z X x H y H z = x H y H z x H y G z = x H y G x H z x G y H z = x H z G y H z x X y X x H y = y y H x = y

Proof

Step Hyp Ref Expression
1 ringi.1 G = 1 st R
2 ringi.2 H = 2 nd R
3 ringi.3 X = ran G
4 relrngo Rel RingOps
5 1st2nd Rel RingOps R RingOps R = 1 st R 2 nd R
6 4 5 mpan R RingOps R = 1 st R 2 nd R
7 1 2 opeq12i G H = 1 st R 2 nd R
8 6 7 syl6reqr R RingOps G H = R
9 id R RingOps R RingOps
10 8 9 eqeltrd R RingOps G H RingOps
11 2 fvexi H V
12 3 isrngo H V G H RingOps G AbelOp H : X × X X x X y X z X x H y H z = x H y H z x H y G z = x H y G x H z x G y H z = x H z G y H z x X y X x H y = y y H x = y
13 11 12 ax-mp G H RingOps G AbelOp H : X × X X x X y X z X x H y H z = x H y H z x H y G z = x H y G x H z x G y H z = x H z G y H z x X y X x H y = y y H x = y
14 10 13 sylib R RingOps G AbelOp H : X × X X x X y X z X x H y H z = x H y H z x H y G z = x H y G x H z x G y H z = x H z G y H z x X y X x H y = y y H x = y