Metamath Proof Explorer

Theorem iscringd

Description: Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses iscringd.1 
|- ( ph -> G e. AbelOp )
iscringd.2 
|- ( ph -> X = ran G )
iscringd.3 
|- ( ph -> H : ( X X. X ) --> X )
iscringd.4 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )
iscringd.5 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) )
iscringd.6 
|- ( ph -> U e. X )
iscringd.7 
|- ( ( ph /\ y e. X ) -> ( y H U ) = y )
iscringd.8 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x H y ) = ( y H x ) )
Assertion iscringd 
|- ( ph -> <. G , H >. e. CRingOps )

Proof

Step Hyp Ref Expression
1 iscringd.1 
 |-  ( ph -> G e. AbelOp )
2 iscringd.2 
 |-  ( ph -> X = ran G )
3 iscringd.3 
 |-  ( ph -> H : ( X X. X ) --> X )
4 iscringd.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )
5 iscringd.5 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) )
6 iscringd.6 
 |-  ( ph -> U e. X )
7 iscringd.7 
 |-  ( ( ph /\ y e. X ) -> ( y H U ) = y )
8 iscringd.8 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x H y ) = ( y H x ) )
9 id 
 |-  ( ( z e. X /\ y e. X /\ x e. X ) -> ( z e. X /\ y e. X /\ x e. X ) )
10 9 3com13 
 |-  ( ( x e. X /\ y e. X /\ z e. X ) -> ( z e. X /\ y e. X /\ x e. X ) )
11 eleq1 
 |-  ( w = z -> ( w e. X <-> z e. X ) )
12 11 3anbi1d 
 |-  ( w = z -> ( ( w e. X /\ y e. X /\ x e. X ) <-> ( z e. X /\ y e. X /\ x e. X ) ) )
13 12 anbi2d 
 |-  ( w = z -> ( ( ph /\ ( w e. X /\ y e. X /\ x e. X ) ) <-> ( ph /\ ( z e. X /\ y e. X /\ x e. X ) ) ) )
14 oveq2 
 |-  ( w = z -> ( ( x G y ) H w ) = ( ( x G y ) H z ) )
15 oveq2 
 |-  ( w = z -> ( x H w ) = ( x H z ) )
16 oveq2 
 |-  ( w = z -> ( y H w ) = ( y H z ) )
17 15 16 oveq12d 
 |-  ( w = z -> ( ( x H w ) G ( y H w ) ) = ( ( x H z ) G ( y H z ) ) )
18 14 17 eqeq12d 
 |-  ( w = z -> ( ( ( x G y ) H w ) = ( ( x H w ) G ( y H w ) ) <-> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) )
19 13 18 imbi12d 
 |-  ( w = z -> ( ( ( ph /\ ( w e. X /\ y e. X /\ x e. X ) ) -> ( ( x G y ) H w ) = ( ( x H w ) G ( y H w ) ) ) <-> ( ( ph /\ ( z e. X /\ y e. X /\ x e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) ) )
20 eleq1 
 |-  ( z = x -> ( z e. X <-> x e. X ) )
21 20 3anbi3d 
 |-  ( z = x -> ( ( w e. X /\ y e. X /\ z e. X ) <-> ( w e. X /\ y e. X /\ x e. X ) ) )
22 21 anbi2d 
 |-  ( z = x -> ( ( ph /\ ( w e. X /\ y e. X /\ z e. X ) ) <-> ( ph /\ ( w e. X /\ y e. X /\ x e. X ) ) ) )
23 oveq1 
 |-  ( z = x -> ( z G y ) = ( x G y ) )
24 23 oveq1d 
 |-  ( z = x -> ( ( z G y ) H w ) = ( ( x G y ) H w ) )
25 oveq1 
 |-  ( z = x -> ( z H w ) = ( x H w ) )
26 25 oveq1d 
 |-  ( z = x -> ( ( z H w ) G ( y H w ) ) = ( ( x H w ) G ( y H w ) ) )
27 24 26 eqeq12d 
 |-  ( z = x -> ( ( ( z G y ) H w ) = ( ( z H w ) G ( y H w ) ) <-> ( ( x G y ) H w ) = ( ( x H w ) G ( y H w ) ) ) )
28 22 27 imbi12d 
 |-  ( z = x -> ( ( ( ph /\ ( w e. X /\ y e. X /\ z e. X ) ) -> ( ( z G y ) H w ) = ( ( z H w ) G ( y H w ) ) ) <-> ( ( ph /\ ( w e. X /\ y e. X /\ x e. X ) ) -> ( ( x G y ) H w ) = ( ( x H w ) G ( y H w ) ) ) ) )
29 eleq1 
 |-  ( x = w -> ( x e. X <-> w e. X ) )
30 29 3anbi1d 
 |-  ( x = w -> ( ( x e. X /\ y e. X /\ z e. X ) <-> ( w e. X /\ y e. X /\ z e. X ) ) )
31 30 anbi2d 
 |-  ( x = w -> ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) <-> ( ph /\ ( w e. X /\ y e. X /\ z e. X ) ) ) )
32 oveq2 
 |-  ( x = w -> ( ( z G y ) H x ) = ( ( z G y ) H w ) )
33 oveq2 
 |-  ( x = w -> ( z H x ) = ( z H w ) )
34 oveq2 
 |-  ( x = w -> ( y H x ) = ( y H w ) )
35 33 34 oveq12d 
 |-  ( x = w -> ( ( z H x ) G ( y H x ) ) = ( ( z H w ) G ( y H w ) ) )
36 32 35 eqeq12d 
 |-  ( x = w -> ( ( ( z G y ) H x ) = ( ( z H x ) G ( y H x ) ) <-> ( ( z G y ) H w ) = ( ( z H w ) G ( y H w ) ) ) )
37 31 36 imbi12d 
 |-  ( x = w -> ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z G y ) H x ) = ( ( z H x ) G ( y H x ) ) ) <-> ( ( ph /\ ( w e. X /\ y e. X /\ z e. X ) ) -> ( ( z G y ) H w ) = ( ( z H w ) G ( y H w ) ) ) ) )
38 1 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> G e. AbelOp )
39 simpr3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> z e. X )
40 2 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> X = ran G )
41 39 40 eleqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> z e. ran G )
42 simpr2 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> y e. X )
43 42 40 eleqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> y e. ran G )
44 eqid 
 |-  ran G = ran G
45 44 ablocom 
 |-  ( ( G e. AbelOp /\ z e. ran G /\ y e. ran G ) -> ( z G y ) = ( y G z ) )
46 38 41 43 45 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z G y ) = ( y G z ) )
47 46 oveq1d 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z G y ) H x ) = ( ( y G z ) H x ) )
48 simpr1 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> x e. X )
49 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
50 38 49 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> G e. GrpOp )
51 44 grpocl 
 |-  ( ( G e. GrpOp /\ y e. ran G /\ z e. ran G ) -> ( y G z ) e. ran G )
52 50 43 41 51 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( y G z ) e. ran G )
53 52 40 eleqtrrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( y G z ) e. X )
54 48 53 jca 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x e. X /\ ( y G z ) e. X ) )
55 ovex 
 |-  ( y G z ) e. _V
56 eleq1 
 |-  ( w = ( y G z ) -> ( w e. X <-> ( y G z ) e. X ) )
57 56 anbi2d 
 |-  ( w = ( y G z ) -> ( ( x e. X /\ w e. X ) <-> ( x e. X /\ ( y G z ) e. X ) ) )
58 57 anbi2d 
 |-  ( w = ( y G z ) -> ( ( ph /\ ( x e. X /\ w e. X ) ) <-> ( ph /\ ( x e. X /\ ( y G z ) e. X ) ) ) )
59 oveq2 
 |-  ( w = ( y G z ) -> ( x H w ) = ( x H ( y G z ) ) )
60 oveq1 
 |-  ( w = ( y G z ) -> ( w H x ) = ( ( y G z ) H x ) )
61 59 60 eqeq12d 
 |-  ( w = ( y G z ) -> ( ( x H w ) = ( w H x ) <-> ( x H ( y G z ) ) = ( ( y G z ) H x ) ) )
62 58 61 imbi12d 
 |-  ( w = ( y G z ) -> ( ( ( ph /\ ( x e. X /\ w e. X ) ) -> ( x H w ) = ( w H x ) ) <-> ( ( ph /\ ( x e. X /\ ( y G z ) e. X ) ) -> ( x H ( y G z ) ) = ( ( y G z ) H x ) ) ) )
63 eleq1 
 |-  ( y = w -> ( y e. X <-> w e. X ) )
64 63 anbi2d 
 |-  ( y = w -> ( ( x e. X /\ y e. X ) <-> ( x e. X /\ w e. X ) ) )
65 64 anbi2d 
 |-  ( y = w -> ( ( ph /\ ( x e. X /\ y e. X ) ) <-> ( ph /\ ( x e. X /\ w e. X ) ) ) )
66 oveq2 
 |-  ( y = w -> ( x H y ) = ( x H w ) )
67 oveq1 
 |-  ( y = w -> ( y H x ) = ( w H x ) )
68 66 67 eqeq12d 
 |-  ( y = w -> ( ( x H y ) = ( y H x ) <-> ( x H w ) = ( w H x ) ) )
69 65 68 imbi12d 
 |-  ( y = w -> ( ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x H y ) = ( y H x ) ) <-> ( ( ph /\ ( x e. X /\ w e. X ) ) -> ( x H w ) = ( w H x ) ) ) )
70 69 8 chvarvv 
 |-  ( ( ph /\ ( x e. X /\ w e. X ) ) -> ( x H w ) = ( w H x ) )
71 55 62 70 vtocl 
 |-  ( ( ph /\ ( x e. X /\ ( y G z ) e. X ) ) -> ( x H ( y G z ) ) = ( ( y G z ) H x ) )
72 54 71 syldan 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( y G z ) H x ) )
73 8 3adantr3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H y ) = ( y H x ) )
74 eleq1 
 |-  ( y = z -> ( y e. X <-> z e. X ) )
75 74 anbi2d 
 |-  ( y = z -> ( ( x e. X /\ y e. X ) <-> ( x e. X /\ z e. X ) ) )
76 75 anbi2d 
 |-  ( y = z -> ( ( ph /\ ( x e. X /\ y e. X ) ) <-> ( ph /\ ( x e. X /\ z e. X ) ) ) )
77 oveq2 
 |-  ( y = z -> ( x H y ) = ( x H z ) )
78 oveq1 
 |-  ( y = z -> ( y H x ) = ( z H x ) )
79 77 78 eqeq12d 
 |-  ( y = z -> ( ( x H y ) = ( y H x ) <-> ( x H z ) = ( z H x ) ) )
80 76 79 imbi12d 
 |-  ( y = z -> ( ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x H y ) = ( y H x ) ) <-> ( ( ph /\ ( x e. X /\ z e. X ) ) -> ( x H z ) = ( z H x ) ) ) )
81 80 8 chvarvv 
 |-  ( ( ph /\ ( x e. X /\ z e. X ) ) -> ( x H z ) = ( z H x ) )
82 81 3adantr2 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H z ) = ( z H x ) )
83 73 82 oveq12d 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) G ( x H z ) ) = ( ( y H x ) G ( z H x ) ) )
84 3 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> H : ( X X. X ) --> X )
85 84 42 48 fovrnd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( y H x ) e. X )
86 85 40 eleqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( y H x ) e. ran G )
87 84 39 48 fovrnd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z H x ) e. X )
88 87 40 eleqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z H x ) e. ran G )
89 44 ablocom 
 |-  ( ( G e. AbelOp /\ ( y H x ) e. ran G /\ ( z H x ) e. ran G ) -> ( ( y H x ) G ( z H x ) ) = ( ( z H x ) G ( y H x ) ) )
90 38 86 88 89 syl3anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( y H x ) G ( z H x ) ) = ( ( z H x ) G ( y H x ) ) )
91 5 83 90 3eqtrd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( z H x ) G ( y H x ) ) )
92 47 72 91 3eqtr2d 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z G y ) H x ) = ( ( z H x ) G ( y H x ) ) )
93 37 92 chvarvv 
 |-  ( ( ph /\ ( w e. X /\ y e. X /\ z e. X ) ) -> ( ( z G y ) H w ) = ( ( z H w ) G ( y H w ) ) )
94 28 93 chvarvv 
 |-  ( ( ph /\ ( w e. X /\ y e. X /\ x e. X ) ) -> ( ( x G y ) H w ) = ( ( x H w ) G ( y H w ) ) )
95 19 94 chvarvv 
 |-  ( ( ph /\ ( z e. X /\ y e. X /\ x e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )
96 10 95 sylan2 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )
97 6 adantr 
 |-  ( ( ph /\ y e. X ) -> U e. X )
98 oveq1 
 |-  ( x = U -> ( x H y ) = ( U H y ) )
99 oveq2 
 |-  ( x = U -> ( y H x ) = ( y H U ) )
100 98 99 eqeq12d 
 |-  ( x = U -> ( ( x H y ) = ( y H x ) <-> ( U H y ) = ( y H U ) ) )
101 100 imbi2d 
 |-  ( x = U -> ( ( ( ph /\ y e. X ) -> ( x H y ) = ( y H x ) ) <-> ( ( ph /\ y e. X ) -> ( U H y ) = ( y H U ) ) ) )
102 8 an12s 
 |-  ( ( x e. X /\ ( ph /\ y e. X ) ) -> ( x H y ) = ( y H x ) )
103 102 ex 
 |-  ( x e. X -> ( ( ph /\ y e. X ) -> ( x H y ) = ( y H x ) ) )
104 101 103 vtoclga 
 |-  ( U e. X -> ( ( ph /\ y e. X ) -> ( U H y ) = ( y H U ) ) )
105 97 104 mpcom 
 |-  ( ( ph /\ y e. X ) -> ( U H y ) = ( y H U ) )
106 105 7 eqtrd 
 |-  ( ( ph /\ y e. X ) -> ( U H y ) = y )
107 1 2 3 4 5 96 6 106 7 isrngod 
 |-  ( ph -> <. G , H >. e. RingOps )
108 2 eleq2d 
 |-  ( ph -> ( x e. X <-> x e. ran G ) )
109 2 eleq2d 
 |-  ( ph -> ( y e. X <-> y e. ran G ) )
110 108 109 anbi12d 
 |-  ( ph -> ( ( x e. X /\ y e. X ) <-> ( x e. ran G /\ y e. ran G ) ) )
111 110 biimpar 
 |-  ( ( ph /\ ( x e. ran G /\ y e. ran G ) ) -> ( x e. X /\ y e. X ) )
112 111 8 syldan 
 |-  ( ( ph /\ ( x e. ran G /\ y e. ran G ) ) -> ( x H y ) = ( y H x ) )
113 112 ralrimivva 
 |-  ( ph -> A. x e. ran G A. y e. ran G ( x H y ) = ( y H x ) )
114 rnexg 
 |-  ( G e. AbelOp -> ran G e. _V )
115 1 114 syl 
 |-  ( ph -> ran G e. _V )
116 2 115 eqeltrd 
 |-  ( ph -> X e. _V )
117 116 116 xpexd 
 |-  ( ph -> ( X X. X ) e. _V )
118 3 117 fexd 
 |-  ( ph -> H e. _V )
119 iscom2 
 |-  ( ( G e. AbelOp /\ H e. _V ) -> ( <. G , H >. e. Com2 <-> A. x e. ran G A. y e. ran G ( x H y ) = ( y H x ) ) )
120 1 118 119 syl2anc 
 |-  ( ph -> ( <. G , H >. e. Com2 <-> A. x e. ran G A. y e. ran G ( x H y ) = ( y H x ) ) )
121 113 120 mpbird 
 |-  ( ph -> <. G , H >. e. Com2 )
122 iscrngo 
 |-  ( <. G , H >. e. CRingOps <-> ( <. G , H >. e. RingOps /\ <. G , H >. e. Com2 ) )
123 107 121 122 sylanbrc 
 |-  ( ph -> <. G , H >. e. CRingOps )